let H, F 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 )
A1: 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 A2: 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 A3: ( len H = n & H = F ^ sq ) ; :: thesis: H = F
A4: (len F) + (len sq) = len (F ^ sq) by FINSEQ_1:35;
A5: dom F = Seg (len F) by FINSEQ_1:def 3;
( 1 <= 1 & 1 <= len F ) by Thlen01;
then A6: 1 in dom F by A5, FINSEQ_1:3;

A7: now

assume H is atomic ; :: thesis: H = F
then consider k being Nat such that
A8: H = atom. k by Def14;
A9: len H = 1 by A8, FINSEQ_1:57;
then ( len F <= 1 & 1 <= len F ) by A3, A4, Thlen01, NAT_1:11;
then 1 + (len sq) = 1 + 0 by A3, A4, A9, XXREAL_0:1;
then sq = {} ;
hence H = F by A3, FINSEQ_1:47; :: thesis: verum

end;

A10: now

assume A11: H is negative ; :: thesis: H = F
then consider H1 being LTL-formula such that
A12: H = 'not' H1 by Def15;
(F ^ sq) . 1 = 0 by A3, A11, Lm3;
then F . 1 = 0 by A6, FINSEQ_1:def 7;
then F is negative by Lm9;
then consider F1 being LTL-formula such that
A13: F = 'not' F1 by Def15;
( 'not' H1 = <*0 *> ^ H1 & 'not' F1 = <*0 *> ^ F1 & (<*0 *> ^ F1) ^ sq = <*0 *> ^ (F1 ^ sq) ) by FINSEQ_1:45;
then A14: H1 = F1 ^ sq by A3, A12, A13, FINSEQ_1:46;
( (len <*0 *>) + (len H1) = len H & (len H1) + 1 = 1 + (len H1) & len <*0 *> = 1 ) by A12, FINSEQ_1:35, FINSEQ_1:57;
then len H1 < len H by NAT_1:13;
hence H = F by A2, A3, A12, A13, A14; :: thesis: verum

end;

A15: now

assume A16: H is conjunctive ; :: thesis: H = F
then consider G1, G being LTL-formula such that
A17: H = G1 '&' G by Def16;
(F ^ sq) . 1 = 1 by A3, A16, Lm4;
then F . 1 = 1 by A6, FINSEQ_1:def 7;
then F is conjunctive by Lm9;
then consider F1, H1 being LTL-formula such that
A18: F = F1 '&' H1 by Def16;
( G1 '&' G = (<*1*> ^ G1) ^ G & F1 '&' H1 = (<*1*> ^ F1) ^ H1 & (<*1*> ^ G1) ^ G = <*1*> ^ (G1 ^ G) & (<*1*> ^ F1) ^ H1 = <*1*> ^ (F1 ^ H1) & (<*1*> ^ (F1 ^ H1)) ^ sq = <*1*> ^ ((F1 ^ H1) ^ sq) & (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) ) by FINSEQ_1:45;
then A19: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A17, A18, FINSEQ_1:46;
then A20: ( ( len G1 <= len F1 or len F1 <= len G1 ) & ( len F1 <= len G1 implies ex sq' being FinSequence st G1 = F1 ^ sq' ) & ( len G1 <= len F1 implies ex sq' being FinSequence st F1 = G1 ^ sq' ) ) by FINSEQ_1:64;

A21: now

given sq' being FinSequence such that A22: G1 = F1 ^ sq' ; :: thesis: G1 = F1
( (len (<*1*> ^ G1)) + (len G) = len H & len (<*1*> ^ G1) = (len <*1*>) + (len G1) & len <*1*> = 1 & 1 + (len G1) = (len G1) + 1 ) by A17, FINSEQ_1:35, FINSEQ_1:57;
then (len G1) + 1 <= len H by NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A2, A3, A22; :: thesis: verum

end;

A23: now

given sq' being FinSequence such that A24: F1 = G1 ^ sq' ; :: thesis: F1 = G1
( len (F ^ sq) = (len F) + (len sq) & len <*1*> = 1 & len (<*1*> ^ F1) = (len <*1*>) + (len F1) & 1 + (len F1) = (len F1) + 1 & len F = (len (<*1*> ^ F1)) + (len H1) & len <*1*> = 1 & (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ) by A18, FINSEQ_1:35, FINSEQ_1:57;
then (len F1) + 1 <= len H by A3, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A2, A3, A24; :: thesis: verum

end;

then A25: G = H1 ^ sq by A19, A20, A21, FINSEQ_1:46;
( (len (<*1*> ^ G1)) + (len G) = len H & len (<*1*> ^ G1) = (len <*1*>) + (len G1) & len <*1*> = 1 & (1 + (len G1)) + (len G) = (len G) + (1 + (len G1)) & (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ) by A17, FINSEQ_1:35, FINSEQ_1:57;
then (len G) + 1 <= len H by NAT_1:11;
then len G < len H by NAT_1:13;
hence H = F by A2, A3, A17, A18, A20, A21, A23, A25; :: thesis: verum

end;

A1501: now

assume A1601: H is disjunctive ; :: thesis: H = F
then consider G1, G being LTL-formula such that
A1701: H = G1 'or' G by Def17;
(F ^ sq) . 1 = 2 by A3, A1601, Lm5;
then F . 1 = 2 by A6, FINSEQ_1:def 7;
then F is disjunctive by Lm9;
then consider F1, H1 being LTL-formula such that
A1801: F = F1 'or' H1 by Def17;
( G1 'or' G = (<*2*> ^ G1) ^ G & F1 'or' H1 = (<*2*> ^ F1) ^ H1 & (<*2*> ^ G1) ^ G = <*2*> ^ (G1 ^ G) & (<*2*> ^ F1) ^ H1 = <*2*> ^ (F1 ^ H1) & (<*2*> ^ (F1 ^ H1)) ^ sq = <*2*> ^ ((F1 ^ H1) ^ sq) & (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) ) by FINSEQ_1:45;
then A1901: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A1701, A1801, FINSEQ_1:46;
then A2001: ( ( len G1 <= len F1 or len F1 <= len G1 ) & ( len F1 <= len G1 implies ex sq' being FinSequence st G1 = F1 ^ sq' ) & ( len G1 <= len F1 implies ex sq' being FinSequence st F1 = G1 ^ sq' ) ) by FINSEQ_1:64;

A2101: now

given sq' being FinSequence such that A2201: G1 = F1 ^ sq' ; :: thesis: G1 = F1
( (len (<*2*> ^ G1)) + (len G) = len H & len (<*2*> ^ G1) = (len <*2*>) + (len G1) & len <*2*> = 1 & 1 + (len G1) = (len G1) + 1 ) by A1701, FINSEQ_1:35, FINSEQ_1:57;
then (len G1) + 1 <= len H by NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A2, A3, A2201; :: thesis: verum

end;

A2301: now

given sq' being FinSequence such that A2401: F1 = G1 ^ sq' ; :: thesis: F1 = G1
( len (F ^ sq) = (len F) + (len sq) & len <*2*> = 1 & len (<*2*> ^ F1) = (len <*2*>) + (len F1) & 1 + (len F1) = (len F1) + 1 & len F = (len (<*2*> ^ F1)) + (len H1) & len <*2*> = 1 & (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ) by A1801, FINSEQ_1:35, FINSEQ_1:57;
then (len F1) + 1 <= len H by A3, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A2, A3, A2401; :: thesis: verum

end;

then A2501: G = H1 ^ sq by A1901, A2001, A2101, FINSEQ_1:46;
( (len (<*2*> ^ G1)) + (len G) = len H & len (<*2*> ^ G1) = (len <*2*>) + (len G1) & len <*2*> = 1 & (1 + (len G1)) + (len G) = (len G) + (1 + (len G1)) & (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ) by A1701, FINSEQ_1:35, FINSEQ_1:57;
then (len G) + 1 <= len H by NAT_1:11;
then len G < len H by NAT_1:13;
hence H = F by A2, A3, A1701, A1801, A2001, A2101, A2301, A2501; :: thesis: verum

end;

A31: now

assume A32: H is next ; :: thesis: H = F
then consider H1 being LTL-formula such that
A33: H = 'X' H1 by Def18;
(F ^ sq) . 1 = 3 by A3, A32, Lm6;
then F . 1 = 3 by A6, FINSEQ_1:def 7;
then F is next by Lm9;
then consider F1 being LTL-formula such that
A34: F = 'X' F1 by Def18;
( 'X' H1 = <*3*> ^ H1 & 'X' F1 = <*3*> ^ F1 & (<*3*> ^ F1) ^ sq = <*3*> ^ (F1 ^ sq) ) by FINSEQ_1:45;
then A35: H1 = F1 ^ sq by A3, A33, A34, FINSEQ_1:46;
( (len <*3*>) + (len H1) = len H & (len H1) + 1 = 1 + (len H1) & len <*3*> = 1 ) by A33, FINSEQ_1:35, FINSEQ_1:57;
then len H1 < len H by NAT_1:13;
hence H = F by A2, A3, A33, A34, A35; :: thesis: verum

end;

A1036: now

assume A36: H is Until ; :: thesis: H = F
then consider G1, G being LTL-formula such that
A37: H = G1 'U' G by Def19;
(F ^ sq) . 1 = 4 by A3, A36, Lm7;
then F . 1 = 4 by A6, FINSEQ_1:def 7;
then F is Until by Lm9;
then consider F1, H1 being LTL-formula such that
A38: F = F1 'U' H1 by Def19;
( G1 'U' G = (<*4*> ^ G1) ^ G & F1 'U' H1 = (<*4*> ^ F1) ^ H1 & (<*4*> ^ G1) ^ G = <*4*> ^ (G1 ^ G) & (<*4*> ^ F1) ^ H1 = <*4*> ^ (F1 ^ H1) & (<*4*> ^ (F1 ^ H1)) ^ sq = <*4*> ^ ((F1 ^ H1) ^ sq) & (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) ) by FINSEQ_1:45;
then A39: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A37, A38, FINSEQ_1:46;
then A40: ( ( len G1 <= len F1 or len F1 <= len G1 ) & ( len F1 <= len G1 implies ex sq' being FinSequence st G1 = F1 ^ sq' ) & ( len G1 <= len F1 implies ex sq' being FinSequence st F1 = G1 ^ sq' ) ) by FINSEQ_1:64;

A41: now

given sq' being FinSequence such that A42: G1 = F1 ^ sq' ; :: thesis: G1 = F1
( (len (<*4*> ^ G1)) + (len G) = len H & len (<*4*> ^ G1) = (len <*4*>) + (len G1) & len <*4*> = 1 & 1 + (len G1) = (len G1) + 1 ) by A37, FINSEQ_1:35, FINSEQ_1:57;
then (len G1) + 1 <= len H by NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A2, A3, A42; :: thesis: verum

end;

A43: now

given sq' being FinSequence such that A44: F1 = G1 ^ sq' ; :: thesis: F1 = G1
( len (F ^ sq) = (len F) + (len sq) & len <*4*> = 1 & len (<*4*> ^ F1) = (len <*4*>) + (len F1) & 1 + (len F1) = (len F1) + 1 & len F = (len (<*4*> ^ F1)) + (len H1) & len <*4*> = 1 & (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ) by A38, FINSEQ_1:35, FINSEQ_1:57;
then (len F1) + 1 <= len H by A3, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A2, A3, A44; :: thesis: verum

end;

then A45: G = H1 ^ sq by A39, A40, A41, FINSEQ_1:46;
( (len (<*4*> ^ G1)) + (len G) = len H & len (<*4*> ^ G1) = (len <*4*>) + (len G1) & len <*4*> = 1 & (1 + (len G1)) + (len G) = (len G) + (1 + (len G1)) & (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ) by A37, FINSEQ_1:35, FINSEQ_1:57;
then (len G) + 1 <= len H by NAT_1:11;
then len G < len H by NAT_1:13;
hence H = F by A2, A3, A37, A38, A40, A41, A43, A45; :: thesis: verum

end;

now

assume A3601: H is Release ; :: thesis: H = F
then consider G1, G being LTL-formula such that
A3701: H = G1 'R' G by Def1901;
(F ^ sq) . 1 = 5 by A3, A3601, Lm701;
then F . 1 = 5 by A6, FINSEQ_1:def 7;
then F is Release by Lm9;
then consider F1, H1 being LTL-formula such that
A3801: F = F1 'R' H1 by Def1901;
( G1 'R' G = (<*5*> ^ G1) ^ G & F1 'R' H1 = (<*5*> ^ F1) ^ H1 & (<*5*> ^ G1) ^ G = <*5*> ^ (G1 ^ G) & (<*5*> ^ F1) ^ H1 = <*5*> ^ (F1 ^ H1) & (<*5*> ^ (F1 ^ H1)) ^ sq = <*5*> ^ ((F1 ^ H1) ^ sq) & (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) ) by FINSEQ_1:45;
then A3901: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A3701, A3801, FINSEQ_1:46;
then A4001: ( ( len G1 <= len F1 or len F1 <= len G1 ) & ( len F1 <= len G1 implies ex sq' being FinSequence st G1 = F1 ^ sq' ) & ( len G1 <= len F1 implies ex sq' being FinSequence st F1 = G1 ^ sq' ) ) by FINSEQ_1:64;

A4101: now

given sq' being FinSequence such that A4201: G1 = F1 ^ sq' ; :: thesis: G1 = F1
( (len (<*5*> ^ G1)) + (len G) = len H & len (<*5*> ^ G1) = (len <*5*>) + (len G1) & len <*5*> = 1 & 1 + (len G1) = (len G1) + 1 ) by A3701, FINSEQ_1:35, FINSEQ_1:57;
then (len G1) + 1 <= len H by NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A2, A3, A4201; :: thesis: verum

end;

A4301: now

given sq' being FinSequence such that A4401: F1 = G1 ^ sq' ; :: thesis: F1 = G1
( len (F ^ sq) = (len F) + (len sq) & len <*5*> = 1 & len (<*5*> ^ F1) = (len <*5*>) + (len F1) & 1 + (len F1) = (len F1) + 1 & len F = (len (<*5*> ^ F1)) + (len H1) & len <*5*> = 1 & (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ) by A3801, FINSEQ_1:35, FINSEQ_1:57;
then (len F1) + 1 <= len H by A3, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A2, A3, A4401; :: thesis: verum

end;

then A4501: G = H1 ^ sq by A3901, A4001, A4101, FINSEQ_1:46;
( (len (<*5*> ^ G1)) + (len G) = len H & len (<*5*> ^ G1) = (len <*5*>) + (len G1) & len <*5*> = 1 & (1 + (len G1)) + (len G) = (len G) + (1 + (len G1)) & (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ) by A3701, FINSEQ_1:35, FINSEQ_1:57;
then (len G) + 1 <= len H by NAT_1:11;
then len G < len H by NAT_1:13;
hence H = F by A2, A3, A3701, A3801, A4001, A4101, A4301, A4501; :: thesis: verum

end;

hence H = F by A7, A10, A15, A1501, A31, A1036, Th2; :: thesis: verum

end;

defpred S₁[ Nat] means for H, F being LTL-formula
for sq being FinSequence st len H = $1 & H = F ^ sq holds
H = F;
A46: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k] by A1;
A47: for n being Nat holds S₁[n] from NAT_1:sch 4(A46);
len H = len H ;
hence ( H = F ^ sq implies H = F ) by A47; :: thesis: verum