let i1, i2 be Nat; :: thesis: for f being V26() standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1 . 2 <> g2 . 2
let f be V26() standard special_circular_sequence; :: thesis: for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1 . 2 <> g2 . 2
let g1, g2 be FinSequence of (TOP-REAL 2); :: thesis: ( i1 <> i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 implies g1 . 2 <> g2 . 2 )
assume that
A1: i1 <> i2 and
A2: g1 is_a_part>_of f,i1,i2 and
A3: g2 is_a_part<_of f,i1,i2 ; :: thesis: g1 . 2 <> g2 . 2
A4: 1 <= i1 by A2;
A5: i2 + 1 <= len f by A2;
then A6: i2 < len f by NAT_1:13;
A7: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
A8: 1 <= i2 by A2;
A9: i1 + 1 <= len f by A2;
then A10: i1 < len f by NAT_1:13;
A11: 1 <= 1 + i1 by NAT_1:11;
then A12: (len f) -' 1 = (len f) - 1 by A9, XREAL_1:233, XXREAL_0:2;
A13: 1 <= len f by A9, A11, XXREAL_0:2;
now :: thesis: ( ( i1 <= i2 & g1 . 2 <> g2 . 2 ) or ( i1 > i2 & g1 . 2 <> g2 . 2 ) )
per cases ( i1 <= i2 or i1 > i2 ) ;
case A14: i1 <= i2 ; :: thesis: g1 . 2 <> g2 . 2
now :: thesis: ( ( i1 = i2 & contradiction ) or ( i1 < i2 & g1 . 2 <> g2 . 2 ) )
per cases ( i1 = i2 or i1 < i2 ) by A14, XXREAL_0:1;
case A15: i1 < i2 ; :: thesis: g1 . 2 <> g2 . 2
A16: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A10, Th9;
(i1 + 1) - 1 <= (len f) - 1 by A9, XREAL_1:9;
then A17: 1 <= (len f) -' 1 by A4, A12, XXREAL_0:2;
A18: g2 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) by A3, A15, Th28;
now :: thesis: ( ( 1 < i1 & g1 . 2 <> g2 . 2 ) or ( 1 = i1 & g1 . 2 <> g2 . 2 ) )
per cases ( 1 < i1 or 1 = i1 ) by A4, XXREAL_0:1;
case A19: 1 < i1 ; :: thesis: g1 . 2 <> g2 . 2
then 1 + 1 <= (i1 - 1) + 1 by NAT_1:13;
then A20: 2 <= len (mid (f,i1,1)) by A4, A16, XREAL_1:233;
A21: 1 + 1 <= i1 by A19, NAT_1:13;
A22: g2 . 2 = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 by A3, A15, Th28
.= (mid (f,i1,1)) . 2 by A20, FINSEQ_1:64
.= f . ((i1 -' 2) + 1) by A13, A10, A19, A20, FINSEQ_6:118
.= f . ((i1 - (1 + 1)) + 1) by A21, XREAL_1:233
.= f . (i1 - 1)
.= f . (i1 -' 1) by A4, XREAL_1:233 ;
1 + 1 <= i1 by A19, NAT_1:13;
then A23: (1 + 1) - 1 <= i1 - 1 by XREAL_1:9;
then A24: 1 <= i1 -' 1 by NAT_D:39;
i1 + 1 <= i2 by A15, NAT_1:13;
then (1 + i1) - i1 <= i2 - i1 by XREAL_1:9;
then 1 <= i2 -' i1 by NAT_D:39;
then 1 + 1 <= (i2 -' i1) + 1 by XREAL_1:6;
then A25: 2 <= len (mid (f,i1,i2)) by A4, A8, A6, A10, A15, FINSEQ_6:118;
A26: g1 . 2 = (mid (f,i1,i2)) . 2 by A2, A15, Th25
.= f . ((2 + i1) -' 1) by A4, A8, A6, A10, A15, A25, FINSEQ_6:118
.= f . (((1 + 1) + i1) - 1) by NAT_D:37
.= f . (i1 + 1) ;
A27: now :: thesis: ( 1 = i1 -' 1 implies not i1 + 1 = len f )
assume that
A28: 1 = i1 -' 1 and
A29: i1 + 1 = len f ; :: thesis: contradiction
1 = i1 - 1 by A28, NAT_D:39;
hence contradiction by A29, GOBOARD7:34; :: thesis: verum
end;
now :: thesis: ( ( 1 <> i1 -' 1 & g1 . 2 <> g2 . 2 ) or ( i1 + 1 <> len f & g1 . 2 <> g2 . 2 ) )
per cases ( 1 <> i1 -' 1 or i1 + 1 <> len f ) by A27;
case A30: 1 <> i1 -' 1 ; :: thesis: g1 . 2 <> g2 . 2
A31: 1 < i1 + 1 by A4, NAT_1:13;
i1 -' 1 < (i1 -' 1) + 1 by NAT_1:13;
then i1 -' 1 < i1 by A4, XREAL_1:235;
then A32: i1 -' 1 < i1 + 1 by NAT_1:13;
A33: i1 + 1 <= len f by A2;
then i1 -' 1 < len f by A32, XXREAL_0:2;
then A34: f . (i1 -' 1) = f /. (i1 -' 1) by A24, FINSEQ_4:15;
1 < i1 -' 1 by A24, A30, XXREAL_0:1;
then f /. (i1 -' 1) <> f /. (i1 + 1) by A32, A33, GOBOARD7:37;
hence g1 . 2 <> g2 . 2 by A9, A22, A26, A34, A31, FINSEQ_4:15; :: thesis: verum
end;
case A35: i1 + 1 <> len f ; :: thesis: g1 . 2 <> g2 . 2
A36: 1 <= i1 -' 1 by A23, NAT_D:39;
i1 -' 1 < (i1 -' 1) + 1 by NAT_1:13;
then i1 -' 1 < i1 by A4, XREAL_1:235;
then A37: i1 -' 1 < i1 + 1 by NAT_1:13;
then i1 -' 1 < len f by A9, XXREAL_0:2;
then A38: f . (i1 -' 1) = f /. (i1 -' 1) by A36, FINSEQ_4:15;
A39: 1 < i1 + 1 by A4, NAT_1:13;
i1 + 1 < len f by A9, A35, XXREAL_0:1;
then f /. (i1 -' 1) <> f /. (i1 + 1) by A36, A37, GOBOARD7:36;
hence g1 . 2 <> g2 . 2 by A9, A22, A26, A38, A39, FINSEQ_4:15; :: thesis: verum
end;
end;
end;
hence g1 . 2 <> g2 . 2 ; :: thesis: verum
end;
case A40: 1 = i1 ; :: thesis: g1 . 2 <> g2 . 2
len f > 4 by GOBOARD7:34;
then (len f) - 1 > (3 + 1) - 1 by XREAL_1:9;
then i1 + 1 < (len f) -' 1 by A12, A40, XXREAL_0:2;
then A41: f /. (i1 + 1) <> f /. ((len f) -' 1) by A12, A7, A40, GOBOARD7:37;
i1 + 1 <= i2 by A15, NAT_1:13;
then (1 + i1) - i1 <= i2 - i1 by XREAL_1:9;
then 1 <= i2 -' i1 by NAT_D:39;
then 1 + 1 <= (i2 -' i1) + 1 by XREAL_1:6;
then A42: 2 <= len (mid (f,i1,i2)) by A4, A8, A6, A10, A15, FINSEQ_6:118;
A43: f . ((len f) -' 1) = f /. ((len f) -' 1) by A12, A7, A17, FINSEQ_4:15;
A44: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A10, Th9
.= 0 + 1 by A40, XREAL_1:232
.= 1 ;
(i2 + 1) + 1 <= (len f) + 1 by A5, XREAL_1:6;
then A45: ((1 + i2) + 1) - i2 <= ((len f) + 1) - i2 by XREAL_1:9;
A46: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A10, Th9
.= 0 + 1 by A40, XREAL_1:232
.= 1 ;
len g2 = ((len f) + i1) -' i2 by A3, A15, Th28
.= ((len f) + 1) - i2 by A6, A40, NAT_D:37 ;
then A47: g2 . 2 = (mid (f,((len f) -' 1),i2)) . (2 - (len (mid (f,i1,1)))) by A18, A44, A45, FINSEQ_6:108
.= f . ((len f) -' 1) by A8, A12, A7, A6, A17, A46, FINSEQ_6:118 ;
A48: 1 < i1 + 1 by A4, NAT_1:13;
g1 . 2 = (mid (f,i1,i2)) . 2 by A2, A15, Th25
.= f . ((2 + i1) -' 1) by A4, A8, A6, A10, A15, A42, FINSEQ_6:118
.= f . (((1 + 1) + i1) - 1) by NAT_D:37
.= f . (i1 + 1) ;
hence g1 . 2 <> g2 . 2 by A9, A47, A41, A43, A48, FINSEQ_4:15; :: thesis: verum
end;
end;
end;
hence g1 . 2 <> g2 . 2 ; :: thesis: verum
end;
end;
end;
hence g1 . 2 <> g2 . 2 ; :: thesis: verum
end;
case A49: i1 > i2 ; :: thesis: g1 . 2 <> g2 . 2
then i2 + 1 <= i1 by NAT_1:13;
then (1 + i2) - i2 <= i1 - i2 by XREAL_1:9;
then 1 <= i1 -' i2 by NAT_D:39;
then 1 + 1 <= (i1 -' i2) + 1 by XREAL_1:6;
then A50: 2 <= len (mid (f,i1,i2)) by A4, A8, A6, A10, A49, FINSEQ_6:118;
1 < i1 by A8, A49, XXREAL_0:2;
then A51: 1 + 1 <= i1 by NAT_1:13;
A52: g2 . 2 = (mid (f,i1,i2)) . 2 by A3, A49, Th27
.= f . ((i1 -' 2) + 1) by A4, A8, A6, A10, A49, A50, FINSEQ_6:118
.= f . ((i1 - (1 + 1)) + 1) by A51, XREAL_1:233
.= f . (i1 - 1)
.= f . (i1 -' 1) by A4, XREAL_1:233 ;
1 < i1 by A8, A49, XXREAL_0:2;
then 1 + 1 <= i1 by NAT_1:13;
then A53: (1 + 1) - 1 <= i1 - 1 by XREAL_1:9;
then A54: 1 <= i1 -' 1 by NAT_D:39;
A55: (i1 + 1) - 1 <= (len f) - 1 by A9, XREAL_1:9;
then 1 <= (len f) -' 1 by A4, A12, XXREAL_0:2;
then A56: len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1 by A4, A12, A7, A10, A55, FINSEQ_6:118;
A57: (i1 + 1) - 1 <= (len f) - 1 by A9, XREAL_1:9;
A58: g1 = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) by A2, A49, Th26;
A59: now :: thesis: ( ( i1 < (len f) - 1 & g1 . 2 = f . (i1 + 1) ) or ( i1 = (len f) - 1 & g1 . 2 = f . (i1 + 1) ) )
per cases ( i1 < (len f) - 1 or i1 = (len f) - 1 ) by A55, XXREAL_0:1;
case i1 < (len f) - 1 ; :: thesis: g1 . 2 = f . (i1 + 1)
then i1 + 1 <= (len f) -' 1 by A12, NAT_1:13;
then A60: 1 + (i1 + 1) <= 1 + ((len f) -' 1) by XREAL_1:6;
then A61: (1 + (i1 + 1)) - i1 <= (1 + ((len f) -' 1)) - i1 by XREAL_1:9;
((1 + 1) + i1) - i1 <= (1 + ((len f) -' 1)) - i1 by A60, XREAL_1:9;
then 1 + 1 <= 1 + (((len f) -' 1) - i1) ;
then A62: 2 <= len (mid (f,i1,((len f) -' 1))) by A12, A56, A57, XREAL_1:233;
thus g1 . 2 = ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 by A2, A49, Th26
.= (mid (f,i1,((len f) -' 1))) . 2 by A62, FINSEQ_1:64
.= f . (((1 + 1) + i1) - 1) by A4, A12, A7, A57, A61, FINSEQ_6:122
.= f . (i1 + 1) ; :: thesis: verum
end;
case A63: i1 = (len f) - 1 ; :: thesis: g1 . 2 = f . (i1 + 1)
then A64: len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' ((len f) -' 1)) + 1 by A4, A12, A7, FINSEQ_6:118
.= 0 + 1 by XREAL_1:232
.= 1 ;
A65: 1 + 1 <= i2 + 1 by A8, XREAL_1:6;
A66: len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' ((len f) -' 1)) + 1 by A4, A12, A7, A63, FINSEQ_6:118
.= 0 + 1 by XREAL_1:232
.= 1 ;
len g1 = ((((len f) -' 1) + 1) + i2) -' ((len f) -' 1) by A2, A12, A49, A63, Th26
.= (((len f) -' 1) + (1 + i2)) -' ((len f) -' 1)
.= 1 + i2 by NAT_D:34 ;
hence g1 . 2 = (mid (f,1,i2)) . (2 - (len (mid (f,i1,((len f) -' 1))))) by A58, A64, A65, FINSEQ_6:108
.= f . 1 by A8, A13, A6, A66, FINSEQ_6:118
.= f . (i1 + 1) by A63, Th5, NAT_1:11 ;
:: thesis: verum
end;
end;
end;
A67: now :: thesis: ( 1 = i1 -' 1 implies not i1 + 1 = len f )
assume that
A68: 1 = i1 -' 1 and
A69: i1 + 1 = len f ; :: thesis: contradiction
1 = i1 - 1 by A68, NAT_D:39;
hence contradiction by A69, GOBOARD7:34; :: thesis: verum
end;
now :: thesis: ( ( 1 <> i1 -' 1 & g1 . 2 <> g2 . 2 ) or ( i1 + 1 <> len f & g1 . 2 <> g2 . 2 ) )
per cases ( 1 <> i1 -' 1 or i1 + 1 <> len f ) by A67;
case A70: 1 <> i1 -' 1 ; :: thesis: g1 . 2 <> g2 . 2
A71: 1 < i1 + 1 by A4, NAT_1:13;
i1 -' 1 < (i1 -' 1) + 1 by NAT_1:13;
then i1 -' 1 < i1 by A4, XREAL_1:235;
then A72: i1 -' 1 < i1 + 1 by NAT_1:13;
A73: i1 + 1 <= len f by A2;
then i1 -' 1 < len f by A72, XXREAL_0:2;
then A74: f . (i1 -' 1) = f /. (i1 -' 1) by A54, FINSEQ_4:15;
1 < i1 -' 1 by A54, A70, XXREAL_0:1;
then f /. (i1 -' 1) <> f /. (i1 + 1) by A72, A73, GOBOARD7:37;
hence g1 . 2 <> g2 . 2 by A9, A59, A52, A74, A71, FINSEQ_4:15; :: thesis: verum
end;
case A75: i1 + 1 <> len f ; :: thesis: g1 . 2 <> g2 . 2
A76: 1 <= i1 -' 1 by A53, NAT_D:39;
i1 -' 1 < (i1 -' 1) + 1 by NAT_1:13;
then i1 -' 1 < i1 by A4, XREAL_1:235;
then A77: i1 -' 1 < i1 + 1 by NAT_1:13;
then i1 -' 1 < len f by A9, XXREAL_0:2;
then A78: f . (i1 -' 1) = f /. (i1 -' 1) by A76, FINSEQ_4:15;
A79: 1 < i1 + 1 by A4, NAT_1:13;
i1 + 1 < len f by A9, A75, XXREAL_0:1;
then f /. (i1 -' 1) <> f /. (i1 + 1) by A76, A77, GOBOARD7:36;
hence g1 . 2 <> g2 . 2 by A9, A59, A52, A78, A79, FINSEQ_4:15; :: thesis: verum
end;
end;
end;
hence g1 . 2 <> g2 . 2 ; :: thesis: verum
end;
end;
end;
hence g1 . 2 <> g2 . 2 ; :: thesis: verum