let H, F 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 S1[ 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:3;
A6: now
A7: len <*0 *> = 1 by FINSEQ_1:57;
assume A8: H is negative ; :: thesis: H = F
then consider H1 being CTL-formula such that
A9: H = 'not' H1 by Def15;
(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 by Def15;
(len <*0 *>) + (len H1) = len H by A9, FINSEQ_1:35;
then A11: len H1 < len H by A7, NAT_1:13;
(<*0 *> ^ F1) ^ sq = <*0 *> ^ (F1 ^ sq) by FINSEQ_1:45;
then H1 = F1 ^ sq by A3, A9, A10, FINSEQ_1:46;
hence H = F by A1, A2, A9, A10, A11; :: thesis: verum
end;
A12: now
A13: len <*4*> = 1 by FINSEQ_1:57;
assume A14: H is ExistUntill ; :: thesis: H = F
then consider G1, G being CTL-formula such that
A15: H = G1 EU G by Def19;
(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 by Def19;
A17: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A18: len (<*4*> ^ G1) = (len <*4*>) + (len G1) by FINSEQ_1:35;
(len (<*4*> ^ G1)) + (len G) = len H by A15, FINSEQ_1:35;
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:45;
A21: now
A22: len <*4*> = 1 by FINSEQ_1:57;
given sq9 being FinSequence such that A23: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A24: len (<*4*> ^ G1) = (len <*4*>) + (len G1) by FINSEQ_1:35;
(len (<*4*> ^ G1)) + (len G) = len H by A15, FINSEQ_1:35;
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:45;
A26: now
A27: len <*4*> = 1 by FINSEQ_1:57;
A28: len (<*4*> ^ F1) = (len <*4*>) + (len F1) by FINSEQ_1:35;
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:35;
len F = (len (<*4*> ^ F1)) + (len H1) by A16, FINSEQ_1:35;
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:45;
(<*4*> ^ G1) ^ G = <*4*> ^ (G1 ^ G) by FINSEQ_1:45;
then A33: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A15, A16, A32, A25, A20, FINSEQ_1:46;
then ( len F1 <= len G1 implies ex sq9 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:64;
then G = H1 ^ sq by A33, A21, A26, FINSEQ_1:46, FINSEQ_1:64;
hence H = F by A1, A2, A3, A16, A32, A25, A20, A19; :: thesis: verum
end;
A34: now
A35: len <*1*> = 1 by FINSEQ_1:57;
assume A36: H is conjunctive ; :: thesis: H = F
then consider G1, G being CTL-formula such that
A37: H = G1 '&' G by Def16;
(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 by Def16;
A39: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A40: len (<*1*> ^ G1) = (len <*1*>) + (len G1) by FINSEQ_1:35;
(len (<*1*> ^ G1)) + (len G) = len H by A37, FINSEQ_1:35;
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:45;
A43: now
A44: len <*1*> = 1 by FINSEQ_1:57;
given sq9 being FinSequence such that A45: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A46: len (<*1*> ^ G1) = (len <*1*>) + (len G1) by FINSEQ_1:35;
(len (<*1*> ^ G1)) + (len G) = len H by A37, FINSEQ_1:35;
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:45;
A48: now
A49: len (<*1*> ^ F1) = (len <*1*>) + (len F1) by FINSEQ_1:35;
A50: len <*1*> = 1 by FINSEQ_1:57;
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:35;
len F = (len (<*1*> ^ F1)) + (len H1) by A38, FINSEQ_1:35;
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:45;
(<*1*> ^ G1) ^ G = <*1*> ^ (G1 ^ G) by FINSEQ_1:45;
then A55: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A37, A38, A54, A47, A42, FINSEQ_1:46;
then ( len F1 <= len G1 implies ex sq9 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:64;
then G = H1 ^ sq by A55, A43, A48, FINSEQ_1:46, FINSEQ_1:64;
hence H = F by A1, A2, A3, A38, A54, A47, A42, A41; :: thesis: verum
end;
A56: now
A57: len <*3*> = 1 by FINSEQ_1:57;
assume A58: H is ExistGlobal ; :: thesis: H = F
then consider H1 being CTL-formula such that
A59: H = EG H1 by Def18;
(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 by Def18;
(len <*3*>) + (len H1) = len H by A59, FINSEQ_1:35;
then A61: len H1 < len H by A57, NAT_1:13;
(<*3*> ^ F1) ^ sq = <*3*> ^ (F1 ^ sq) by FINSEQ_1:45;
then H1 = F1 ^ sq by A3, A59, A60, FINSEQ_1:46;
hence H = F by A1, A2, A59, A60, A61; :: thesis: verum
end;
A62: now
A63: len <*2*> = 1 by FINSEQ_1:57;
assume A64: H is ExistNext ; :: thesis: H = F
then consider H1 being CTL-formula such that
A65: H = EX H1 by Def17;
(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 by Def17;
(len <*2*>) + (len H1) = len H by A65, FINSEQ_1:35;
then A67: len H1 < len H by A63, NAT_1:13;
(<*2*> ^ F1) ^ sq = <*2*> ^ (F1 ^ sq) by FINSEQ_1:45;
then H1 = F1 ^ sq by A3, A65, A66, FINSEQ_1:46;
hence H = F by A1, A2, A65, A66, A67; :: thesis: verum
end;
A68: (len F) + (len sq) = len (F ^ sq) by FINSEQ_1:35;
now
A69: 1 <= len F by Lm10;
assume H is atomic ; :: thesis: H = F
then ex k being Element of NAT st H = atom. k by Def14;
then A70: len H = 1 by FINSEQ_1:57;
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:47; :: 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
S1[n] ) holds
S1[k] ;
A72: for n being Nat holds S1[n] from NAT_1:sch 4(A71);
 len H = len H ;
hence ( H = F ^ sq implies H = F ) by A72; :: thesis: verum