let F, H be CTL-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 S₁[ Nat] means for H, F being CTL-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 CTL-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ) holds
for H, F being CTL-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 CTL-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ) implies for H, F being CTL-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 CTL-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ; :: thesis: for H, F being CTL-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
let H, F be CTL-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
A4: dom F = Seg (len F) by FINSEQ_1:def 3;
1 <= len F by Lm10;
then A5: 1 in dom F by A4, FINSEQ_1:1;

A6: now :: thesis: ( H is negative implies H = F )

A7: len <*0*> = 1 by FINSEQ_1:40;
assume A8: H is negative ; :: thesis: H = F
then consider H1 being CTL-formula such that
A9: H = 'not' H1 ;
(F ^ sq) . 1 = 0 by A3, A8, Lm3;
then F . 1 = 0 by A5, FINSEQ_1:def 7;
then F is negative by Lm9;
then consider F1 being CTL-formula such that
A10: F = 'not' F1 ;
(len <*0*>) + (len H1) = len H by A9, FINSEQ_1:22;
then A11: len H1 < len H by A7, NAT_1:13;
(<*0*> ^ F1) ^ sq = <*0*> ^ (F1 ^ sq) by FINSEQ_1:32;
then H1 = F1 ^ sq by A3, A9, A10, FINSEQ_1:33;
hence H = F by A1, A2, A9, A10, A11; :: thesis: verum

end;

A12: now :: thesis: ( H is ExistUntill implies H = F )

A13: len <*4*> = 1 by FINSEQ_1:40;
assume A14: H is ExistUntill ; :: thesis: H = F
then consider G1, G being CTL-formula such that
A15: H = G1 EU G ;
(F ^ sq) . 1 = 4 by A3, A14, Lm7;
then F . 1 = 4 by A5, FINSEQ_1:def 7;
then F is ExistUntill by Lm9;
then consider F1, H1 being CTL-formula such that
A16: F = F1 EU H1 ;
A17: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A18: len (<*4*> ^ G1) = (len <*4*>) + (len G1) by FINSEQ_1:22;
(len (<*4*> ^ G1)) + (len G) = len H by A15, FINSEQ_1:22;
then (len G) + 1 <= len H by A18, A13, A17, NAT_1:11;
then A19: len G < len H by NAT_1:13;
A20: (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) by FINSEQ_1:32;

A21: now :: thesis: ( ex sq9 being FinSequence st G1 = F1 ^ sq9 implies G1 = F1 )

A22: len <*4*> = 1 by FINSEQ_1:40;
given sq9 being FinSequence such that A23: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A24: len (<*4*> ^ G1) = (len <*4*>) + (len G1) by FINSEQ_1:22;
(len (<*4*> ^ G1)) + (len G) = len H by A15, FINSEQ_1:22;
then (len G1) + 1 <= len H by A24, A22, NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1, A2, A23; :: thesis: verum

end;

A25: (<*4*> ^ (F1 ^ H1)) ^ sq = <*4*> ^ ((F1 ^ H1) ^ sq) by FINSEQ_1:32;

A26: now :: thesis: ( ex sq9 being FinSequence st F1 = G1 ^ sq9 implies F1 = G1 )

A27: len <*4*> = 1 by FINSEQ_1:40;
A28: len (<*4*> ^ F1) = (len <*4*>) + (len F1) by FINSEQ_1:22;
A29: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ;
given sq9 being FinSequence such that A30: F1 = G1 ^ sq9 ; :: thesis: F1 = G1
A31: len (F ^ sq) = (len F) + (len sq) by FINSEQ_1:22;
len F = (len (<*4*> ^ F1)) + (len H1) by A16, FINSEQ_1:22;
then (len F1) + 1 <= len H by A3, A31, A28, A27, A29, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1, A2, A30; :: thesis: verum

end;

A32: (<*4*> ^ F1) ^ H1 = <*4*> ^ (F1 ^ H1) by FINSEQ_1:32;
(<*4*> ^ G1) ^ G = <*4*> ^ (G1 ^ G) by FINSEQ_1:32;
then A33: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A15, A16, A32, A25, A20, 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 A33, A21, A26, FINSEQ_1:33, FINSEQ_1:47;
hence H = F by A1, A2, A3, A16, A32, A25, A20, A19; :: thesis: verum

end;

A34: now :: thesis: ( H is conjunctive implies H = F )

A35: len <*1*> = 1 by FINSEQ_1:40;
assume A36: H is conjunctive ; :: thesis: H = F
then consider G1, G being CTL-formula such that
A37: H = G1 '&' G ;
(F ^ sq) . 1 = 1 by A3, A36, Lm4;
then F . 1 = 1 by A5, FINSEQ_1:def 7;
then F is conjunctive by Lm9;
then consider F1, H1 being CTL-formula such that
A38: F = F1 '&' H1 ;
A39: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A40: len (<*1*> ^ G1) = (len <*1*>) + (len G1) by FINSEQ_1:22;
(len (<*1*> ^ G1)) + (len G) = len H by A37, FINSEQ_1:22;
then (len G) + 1 <= len H by A40, A35, A39, NAT_1:11;
then A41: len G < len H by NAT_1:13;
A42: (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) by FINSEQ_1:32;

A43: now :: thesis: ( ex sq9 being FinSequence st G1 = F1 ^ sq9 implies G1 = F1 )

A44: len <*1*> = 1 by FINSEQ_1:40;
given sq9 being FinSequence such that A45: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A46: len (<*1*> ^ G1) = (len <*1*>) + (len G1) by FINSEQ_1:22;
(len (<*1*> ^ G1)) + (len G) = len H by A37, FINSEQ_1:22;
then (len G1) + 1 <= len H by A46, A44, NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1, A2, A45; :: thesis: verum

end;

A47: (<*1*> ^ (F1 ^ H1)) ^ sq = <*1*> ^ ((F1 ^ H1) ^ sq) by FINSEQ_1:32;

A48: now :: thesis: ( ex sq9 being FinSequence st F1 = G1 ^ sq9 implies F1 = G1 )

A49: len (<*1*> ^ F1) = (len <*1*>) + (len F1) by FINSEQ_1:22;
A50: len <*1*> = 1 by FINSEQ_1:40;
A51: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ;
given sq9 being FinSequence such that A52: F1 = G1 ^ sq9 ; :: thesis: F1 = G1
A53: len (F ^ sq) = (len F) + (len sq) by FINSEQ_1:22;
len F = (len (<*1*> ^ F1)) + (len H1) by A38, FINSEQ_1:22;
then (len F1) + 1 <= len H by A3, A53, A50, A49, A51, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1, A2, A52; :: thesis: verum

end;

A54: (<*1*> ^ F1) ^ H1 = <*1*> ^ (F1 ^ H1) by FINSEQ_1:32;
(<*1*> ^ G1) ^ G = <*1*> ^ (G1 ^ G) by FINSEQ_1:32;
then A55: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A37, A38, A54, A47, A42, 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 A55, A43, A48, FINSEQ_1:33, FINSEQ_1:47;
hence H = F by A1, A2, A3, A38, A54, A47, A42, A41; :: thesis: verum

end;

A56: now :: thesis: ( H is ExistGlobal implies H = F )

A57: len <*3*> = 1 by FINSEQ_1:40;
assume A58: H is ExistGlobal ; :: thesis: H = F
then consider H1 being CTL-formula such that
A59: H = EG H1 ;
(F ^ sq) . 1 = 3 by A3, A58, Lm6;
then F . 1 = 3 by A5, FINSEQ_1:def 7;
then F is ExistGlobal by Lm9;
then consider F1 being CTL-formula such that
A60: F = EG F1 ;
(len <*3*>) + (len H1) = len H by A59, FINSEQ_1:22;
then A61: len H1 < len H by A57, NAT_1:13;
(<*3*> ^ F1) ^ sq = <*3*> ^ (F1 ^ sq) by FINSEQ_1:32;
then H1 = F1 ^ sq by A3, A59, A60, FINSEQ_1:33;
hence H = F by A1, A2, A59, A60, A61; :: thesis: verum

end;

A62: now :: thesis: ( H is ExistNext implies H = F )

A63: len <*2*> = 1 by FINSEQ_1:40;
assume A64: H is ExistNext ; :: thesis: H = F
then consider H1 being CTL-formula such that
A65: H = EX H1 ;
(F ^ sq) . 1 = 2 by A3, A64, Lm5;
then F . 1 = 2 by A5, FINSEQ_1:def 7;
then F is ExistNext by Lm9;
then consider F1 being CTL-formula such that
A66: F = EX F1 ;
(len <*2*>) + (len H1) = len H by A65, FINSEQ_1:22;
then A67: len H1 < len H by A63, NAT_1:13;
(<*2*> ^ F1) ^ sq = <*2*> ^ (F1 ^ sq) by FINSEQ_1:32;
then H1 = F1 ^ sq by A3, A65, A66, FINSEQ_1:33;
hence H = F by A1, A2, A65, A66, A67; :: thesis: verum

end;

A68: (len F) + (len sq) = len (F ^ sq) by FINSEQ_1:22;

now :: thesis: ( H is atomic implies H = F )

A69: 1 <= len F by Lm10;
assume H is atomic ; :: thesis: H = F
then ex k being Element of NAT st H = atom. k ;
then A70: len H = 1 by FINSEQ_1:40;
then len F <= 1 by A3, A68, NAT_1:11;
then 1 + (len sq) = 1 + 0 by A3, A68, A70, A69, XXREAL_0:1;
then sq = {} ;
hence H = F by A3, FINSEQ_1:34; :: thesis: verum

end;

hence H = F by A6, A34, A62, A56, A12, Th2; :: thesis: verum

end;

then A71: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k] ;
A72: for n being Nat holds S₁[n] from NAT_1:sch 4(A71);
len H = len H ;
hence ( H = F ^ sq implies H = F ) by A72; :: thesis: verum