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 )
A1: 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 A2: 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 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 Lm10;
then A6: 1 in dom F by A5, FINSEQ_1:3;
A7: now
assume H is atomic ; :: thesis: H = F
then consider k being Element of 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, Lm10, 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 CTL-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 CTL-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 CTL-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 CTL-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;
A26: now
assume A27: H is ExistNext ; :: thesis: H = F
then consider H1 being CTL-formula such that
A28: H = EX H1 by Def17;
(F ^ sq) . 1 = 2 by A3, A27, Lm5;
then F . 1 = 2 by A6, FINSEQ_1:def 7;
then F is ExistNext by Lm9;
then consider F1 being CTL-formula such that
A29: F = EX F1 by Def17;
( EX H1 = <*2*> ^ H1 & EX F1 = <*2*> ^ F1 & (<*2*> ^ F1) ^ sq = <*2*> ^ (F1 ^ sq) ) by FINSEQ_1:45;
then A30: H1 = F1 ^ sq by A3, A28, A29, FINSEQ_1:46;
( (len <*2*>) + (len H1) = len H & (len H1) + 1 = 1 + (len H1) & len <*2*> = 1 ) by A28, FINSEQ_1:35, FINSEQ_1:57;
then len H1 < len H by NAT_1:13;
hence H = F by A2, A3, A28, A29, A30; :: thesis: verum
end;
A31: now
assume A32: H is ExistGlobal ; :: thesis: H = F
then consider H1 being CTL-formula such that
A33: H = EG H1 by Def18;
(F ^ sq) . 1 = 3 by A3, A32, Lm6;
then F . 1 = 3 by A6, FINSEQ_1:def 7;
then F is ExistGlobal by Lm9;
then consider F1 being CTL-formula such that
A34: F = EG F1 by Def18;
( EG H1 = <*3*> ^ H1 & EG 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;
now
assume A36: H is ExistUntill ; :: thesis: H = F
then consider G1, G being CTL-formula such that
A37: H = G1 EU G by Def19;
(F ^ sq) . 1 = 4 by A3, A36, Lm7;
then F . 1 = 4 by A6, FINSEQ_1:def 7;
then F is ExistUntill by Lm9;
then consider F1, H1 being CTL-formula such that
A38: F = F1 EU H1 by Def19;
( G1 EU G = (<*4*> ^ G1) ^ G & F1 EU 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 <*1*> = 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;
hence H = F by A7, A10, A15, A26, A31, Th2; :: thesis: verum
end;
defpred S1[ Nat] means for H, F being CTL-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
S1[n] ) holds
S1[k] by A1;
A47: for n being Nat holds S1[n] from NAT_1:sch 4(A46);
 len H = len H ;
hence ( H = F ^ sq implies H = F ) by A47; :: thesis: verum