let F, H be LTL-formula; :: thesis: for sq being FinSequence st H = F ^ sq holds
H = F
let sq be FinSequence; :: thesis: ( H = F ^ sq implies H = F )
defpred S1[ Nat] means for H, F being LTL-formula
for sq being FinSequence st len H = $1 & H = F ^ sq holds
H = F;
for n being Nat st ( for k being Nat st k < n holds
for H, F being LTL-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ) holds
for H, F being LTL-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
proof
let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
for H, F being LTL-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ) implies for H, F being LTL-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F )
assume A1: for k being Nat st k < n holds
for H, F being LTL-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ; :: thesis: for H, F being LTL-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
let H, F be LTL-formula; :: thesis: for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
let sq be FinSequence; :: thesis: ( len H = n & H = F ^ sq implies H = F )
assume that
A2: len H = n and
A3: H = F ^ sq ; :: thesis: H = F
( dom F = Seg (len F) & 1 <= len F ) by Th3, FINSEQ_1:def 3;
then A4: 1 in dom F by FINSEQ_1:1;
A5: now :: thesis: ( H is negative implies H = F )
A6: len <*0*> = 1 by FINSEQ_1:40;
assume A7: H is negative ; :: thesis: H = F
then consider H1 being LTL-formula such that
A8: H = 'not' H1 ;
(F ^ sq) . 1 = 0 by A3, A7, Lm3;
then F . 1 = 0 by A4, FINSEQ_1:def 7;
then F is negative by Lm10;
then consider F1 being LTL-formula such that
A9: F = 'not' F1 ;
(len <*0*>) + (len H1) = len H by A8, FINSEQ_1:22;
then A10: len H1 < len H by A6, NAT_1:13;
(<*0*> ^ F1) ^ sq = <*0*> ^ (F1 ^ sq) by FINSEQ_1:32;
then H1 = F1 ^ sq by A3, A8, A9, FINSEQ_1:33;
hence H = F by A1, A2, A8, A9, A10; :: thesis: verum
end;
A11: now :: thesis: ( H is Release implies H = F )
assume A12: H is Release ; :: thesis: H = F
then consider G1, G being LTL-formula such that
A13: H = G1 'R' G ;
A14: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A15: ( len (<*5*> ^ G1) = (len <*5*>) + (len G1) & len <*5*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
(len (<*5*> ^ G1)) + (len G) = len H by A13, FINSEQ_1:22;
then (len G) + 1 <= len H by A15, A14, NAT_1:11;
then A16: len G < len H by NAT_1:13;
(F ^ sq) . 1 = 5 by A3, A12, Lm8;
then F . 1 = 5 by A4, FINSEQ_1:def 7;
then F is Release by Lm10;
then consider F1, H1 being LTL-formula such that
A17: F = F1 'R' H1 ;
A18: now :: thesis: ( ex sq9 being FinSequence st F1 = G1 ^ sq9 implies F1 = G1 )
A19: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ;
given sq9 being FinSequence such that A20: F1 = G1 ^ sq9 ; :: thesis: F1 = G1
A21: ( len (F ^ sq) = (len F) + (len sq) & len <*5*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
( len (<*5*> ^ F1) = (len <*5*>) + (len F1) & len F = (len (<*5*> ^ F1)) + (len H1) ) by A17, FINSEQ_1:22;
then (len F1) + 1 <= len H by A3, A21, A19, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1, A2, A20; :: thesis: verum
end;
A22: ( (<*5*> ^ F1) ^ H1 = <*5*> ^ (F1 ^ H1) & (<*5*> ^ (F1 ^ H1)) ^ sq = <*5*> ^ ((F1 ^ H1) ^ sq) ) by FINSEQ_1:32;
A23: now :: thesis: ( ex sq9 being FinSequence st G1 = F1 ^ sq9 implies G1 = F1 )
given sq9 being FinSequence such that A24: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A25: len <*5*> = 1 by FINSEQ_1:40;
( (len (<*5*> ^ G1)) + (len G) = len H & len (<*5*> ^ G1) = (len <*5*>) + (len G1) ) by A13, FINSEQ_1:22;
then (len G1) + 1 <= len H by A25, NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1, A2, A24; :: thesis: verum
end;
A26: (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) by FINSEQ_1:32;
(<*5*> ^ G1) ^ G = <*5*> ^ (G1 ^ G) by FINSEQ_1:32;
then A27: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A13, A17, A22, A26, FINSEQ_1:33;
then ( len F1 <= len G1 implies ex sq9 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:47;
then G = H1 ^ sq by A27, A23, A18, FINSEQ_1:33, FINSEQ_1:47;
hence H = F by A1, A2, A3, A17, A22, A26, A16; :: thesis: verum
end;
A28: now :: thesis: ( H is Until implies H = F )
assume A29: H is Until ; :: thesis: H = F
then consider G1, G being LTL-formula such that
A30: H = G1 'U' G ;
A31: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A32: ( len (<*4*> ^ G1) = (len <*4*>) + (len G1) & len <*4*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
(len (<*4*> ^ G1)) + (len G) = len H by A30, FINSEQ_1:22;
then (len G) + 1 <= len H by A32, A31, NAT_1:11;
then A33: len G < len H by NAT_1:13;
(F ^ sq) . 1 = 4 by A3, A29, Lm7;
then F . 1 = 4 by A4, FINSEQ_1:def 7;
then F is Until by Lm10;
then consider F1, H1 being LTL-formula such that
A34: F = F1 'U' H1 ;
A35: now :: thesis: ( ex sq9 being FinSequence st F1 = G1 ^ sq9 implies F1 = G1 )
A36: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ;
given sq9 being FinSequence such that A37: F1 = G1 ^ sq9 ; :: thesis: F1 = G1
A38: ( len (F ^ sq) = (len F) + (len sq) & len <*4*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
( len (<*4*> ^ F1) = (len <*4*>) + (len F1) & len F = (len (<*4*> ^ F1)) + (len H1) ) by A34, FINSEQ_1:22;
then (len F1) + 1 <= len H by A3, A38, A36, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1, A2, A37; :: thesis: verum
end;
A39: ( (<*4*> ^ F1) ^ H1 = <*4*> ^ (F1 ^ H1) & (<*4*> ^ (F1 ^ H1)) ^ sq = <*4*> ^ ((F1 ^ H1) ^ sq) ) by FINSEQ_1:32;
A40: now :: thesis: ( ex sq9 being FinSequence st G1 = F1 ^ sq9 implies G1 = F1 )
given sq9 being FinSequence such that A41: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A42: len <*4*> = 1 by FINSEQ_1:40;
( (len (<*4*> ^ G1)) + (len G) = len H & len (<*4*> ^ G1) = (len <*4*>) + (len G1) ) by A30, FINSEQ_1:22;
then (len G1) + 1 <= len H by A42, NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1, A2, A41; :: thesis: verum
end;
A43: (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) by FINSEQ_1:32;
(<*4*> ^ G1) ^ G = <*4*> ^ (G1 ^ G) by FINSEQ_1:32;
then A44: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A30, A34, A39, A43, FINSEQ_1:33;
then ( len F1 <= len G1 implies ex sq9 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:47;
then G = H1 ^ sq by A44, A40, A35, FINSEQ_1:33, FINSEQ_1:47;
hence H = F by A1, A2, A3, A34, A39, A43, A33; :: thesis: verum
end;
A45: now :: thesis: ( H is disjunctive implies H = F )
assume A46: H is disjunctive ; :: thesis: H = F
then consider G1, G being LTL-formula such that
A47: H = G1 'or' G ;
A48: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A49: ( len (<*2*> ^ G1) = (len <*2*>) + (len G1) & len <*2*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
(len (<*2*> ^ G1)) + (len G) = len H by A47, FINSEQ_1:22;
then (len G) + 1 <= len H by A49, A48, NAT_1:11;
then A50: len G < len H by NAT_1:13;
(F ^ sq) . 1 = 2 by A3, A46, Lm5;
then F . 1 = 2 by A4, FINSEQ_1:def 7;
then F is disjunctive by Lm10;
then consider F1, H1 being LTL-formula such that
A51: F = F1 'or' H1 ;
A52: now :: thesis: ( ex sq9 being FinSequence st F1 = G1 ^ sq9 implies F1 = G1 )
A53: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ;
given sq9 being FinSequence such that A54: F1 = G1 ^ sq9 ; :: thesis: F1 = G1
A55: ( len (F ^ sq) = (len F) + (len sq) & len <*2*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
( len (<*2*> ^ F1) = (len <*2*>) + (len F1) & len F = (len (<*2*> ^ F1)) + (len H1) ) by A51, FINSEQ_1:22;
then (len F1) + 1 <= len H by A3, A55, A53, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1, A2, A54; :: thesis: verum
end;
A56: ( (<*2*> ^ F1) ^ H1 = <*2*> ^ (F1 ^ H1) & (<*2*> ^ (F1 ^ H1)) ^ sq = <*2*> ^ ((F1 ^ H1) ^ sq) ) by FINSEQ_1:32;
A57: now :: thesis: ( ex sq9 being FinSequence st G1 = F1 ^ sq9 implies G1 = F1 )
given sq9 being FinSequence such that A58: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A59: len <*2*> = 1 by FINSEQ_1:40;
( (len (<*2*> ^ G1)) + (len G) = len H & len (<*2*> ^ G1) = (len <*2*>) + (len G1) ) by A47, FINSEQ_1:22;
then (len G1) + 1 <= len H by A59, NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1, A2, A58; :: thesis: verum
end;
A60: (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) by FINSEQ_1:32;
(<*2*> ^ G1) ^ G = <*2*> ^ (G1 ^ G) by FINSEQ_1:32;
then A61: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A47, A51, A56, A60, FINSEQ_1:33;
then ( len F1 <= len G1 implies ex sq9 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:47;
then G = H1 ^ sq by A61, A57, A52, FINSEQ_1:33, FINSEQ_1:47;
hence H = F by A1, A2, A3, A51, A56, A60, A50; :: thesis: verum
end;
A62: now :: thesis: ( H is conjunctive implies H = F )
assume A63: H is conjunctive ; :: thesis: H = F
then consider G1, G being LTL-formula such that
A64: H = G1 '&' G ;
A65: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A66: ( len (<*1*> ^ G1) = (len <*1*>) + (len G1) & len <*1*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
(len (<*1*> ^ G1)) + (len G) = len H by A64, FINSEQ_1:22;
then (len G) + 1 <= len H by A66, A65, NAT_1:11;
then A67: len G < len H by NAT_1:13;
(F ^ sq) . 1 = 1 by A3, A63, Lm4;
then F . 1 = 1 by A4, FINSEQ_1:def 7;
then F is conjunctive by Lm10;
then consider F1, H1 being LTL-formula such that
A68: F = F1 '&' H1 ;
A69: now :: thesis: ( ex sq9 being FinSequence st F1 = G1 ^ sq9 implies F1 = G1 )
A70: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ;
given sq9 being FinSequence such that A71: F1 = G1 ^ sq9 ; :: thesis: F1 = G1
A72: ( len (F ^ sq) = (len F) + (len sq) & len <*1*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
( len (<*1*> ^ F1) = (len <*1*>) + (len F1) & len F = (len (<*1*> ^ F1)) + (len H1) ) by A68, FINSEQ_1:22;
then (len F1) + 1 <= len H by A3, A72, A70, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1, A2, A71; :: thesis: verum
end;
A73: ( (<*1*> ^ F1) ^ H1 = <*1*> ^ (F1 ^ H1) & (<*1*> ^ (F1 ^ H1)) ^ sq = <*1*> ^ ((F1 ^ H1) ^ sq) ) by FINSEQ_1:32;
A74: now :: thesis: ( ex sq9 being FinSequence st G1 = F1 ^ sq9 implies G1 = F1 )
given sq9 being FinSequence such that A75: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A76: len <*1*> = 1 by FINSEQ_1:40;
( (len (<*1*> ^ G1)) + (len G) = len H & len (<*1*> ^ G1) = (len <*1*>) + (len G1) ) by A64, FINSEQ_1:22;
then (len G1) + 1 <= len H by A76, NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1, A2, A75; :: thesis: verum
end;
A77: (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) by FINSEQ_1:32;
(<*1*> ^ G1) ^ G = <*1*> ^ (G1 ^ G) by FINSEQ_1:32;
then A78: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A64, A68, A73, A77, FINSEQ_1:33;
then ( len F1 <= len G1 implies ex sq9 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:47;
then G = H1 ^ sq by A78, A74, A69, FINSEQ_1:33, FINSEQ_1:47;
hence H = F by A1, A2, A3, A68, A73, A77, A67; :: thesis: verum
end;
A79: now :: thesis: ( H is next implies H = F )
A80: len <*3*> = 1 by FINSEQ_1:40;
assume A81: H is next ; :: thesis: H = F
then consider H1 being LTL-formula such that
A82: H = 'X' H1 ;
(F ^ sq) . 1 = 3 by A3, A81, Lm6;
then F . 1 = 3 by A4, FINSEQ_1:def 7;
then F is next by Lm10;
then consider F1 being LTL-formula such that
A83: F = 'X' F1 ;
(len <*3*>) + (len H1) = len H by A82, FINSEQ_1:22;
then A84: len H1 < len H by A80, NAT_1:13;
(<*3*> ^ F1) ^ sq = <*3*> ^ (F1 ^ sq) by FINSEQ_1:32;
then H1 = F1 ^ sq by A3, A82, A83, FINSEQ_1:33;
hence H = F by A1, A2, A82, A83, A84; :: thesis: verum
end;
A85: (len F) + (len sq) = len (F ^ sq) by FINSEQ_1:22;
now :: thesis: ( H is atomic implies H = F )
A86: 1 <= len F by Th3;
assume H is atomic ; :: thesis: H = F
then ex k being Nat st H = atom. k ;
then A87: len H = 1 by FINSEQ_1:40;
then len F <= 1 by A3, A85, NAT_1:11;
then 1 + (len sq) = 1 + 0 by A3, A85, A87, A86, XXREAL_0:1;
then sq = {} ;
hence H = F by A3, FINSEQ_1:34; :: thesis: verum
end;
hence H = F by A5, A62, A45, A79, A28, A11, Th2; :: thesis: verum
end;
then A88: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k] ;
A89: for n being Nat holds S1[n] from NAT_1:sch 4(A88);
 len H = len H ;
hence ( H = F ^ sq implies H = F ) by A89; :: thesis: verum