let V be CTLModel; :: thesis: for Kai being Function of atomic_WFF, the BasicAssign of V
for f1, f2 being Function of CTL_WFF, the carrier of V
for n being Nat st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being CTL-formula st len H <= n holds
f1 . H = f2 . H
let Kai be Function of atomic_WFF, the BasicAssign of V; :: thesis: for f1, f2 being Function of CTL_WFF, the carrier of V
for n being Nat st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being CTL-formula st len H <= n holds
f1 . H = f2 . H
let f1, f2 be Function of CTL_WFF, the carrier of V; :: thesis: for n being Nat st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being CTL-formula st len H <= n holds
f1 . H = f2 . H
let n be Nat; :: thesis: ( f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai implies for H being CTL-formula st len H <= n holds
f1 . H = f2 . H )
defpred S₁[ Nat] means ( f1 is-PreEvaluation-for $1,Kai & f2 is-PreEvaluation-for $1,Kai implies for H being CTL-formula st len H <= $1 holds
f1 . H = f2 . H );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
assume that
A3: f1 is-PreEvaluation-for k + 1,Kai and
A4: f2 is-PreEvaluation-for k + 1,Kai ; :: thesis: for H being CTL-formula st len H <= k + 1 holds
f1 . H = f2 . H
let H be CTL-formula; :: thesis: ( len H <= k + 1 implies f1 . H = f2 . H )
assume A5: len H <= k + 1 ; :: thesis: f1 . H = f2 . H

per cases ( H is atomic or H is negative or H is ExistNext or H is ExistGlobal or H is conjunctive or H is ExistUntill ) by Th2;

suppose A6: H is atomic ; :: thesis: f1 . H = f2 . H

then f1 . H = Kai . H by A3, A5;
hence f1 . H = f2 . H by A4, A5, A6; :: thesis: verum

end;

suppose A7: H is negative ; :: thesis: f1 . H = f2 . H

then len (the_argument_of H) < len H by Lm22;
then A8: len (the_argument_of H) <= k by A5, Lm1;
f2 . H = the Compl of V . (f2 . (the_argument_of H)) by A4, A5, A7
.= the Compl of V . (f1 . (the_argument_of H)) by A2, A3, A4, A8, Lm25 ;
hence f1 . H = f2 . H by A3, A5, A7; :: thesis: verum

end;

suppose A9: H is ExistNext ; :: thesis: f1 . H = f2 . H

then len (the_argument_of H) < len H by Lm22;
then A10: len (the_argument_of H) <= k by A5, Lm1;
f2 . H = the EneXt of V . (f2 . (the_argument_of H)) by A4, A5, A9
.= the EneXt of V . (f1 . (the_argument_of H)) by A2, A3, A4, A10, Lm25 ;
hence f1 . H = f2 . H by A3, A5, A9; :: thesis: verum

end;

suppose A11: H is ExistGlobal ; :: thesis: f1 . H = f2 . H

then len (the_argument_of H) < len H by Lm22;
then A12: len (the_argument_of H) <= k by A5, Lm1;
f2 . H = the EGlobal of V . (f2 . (the_argument_of H)) by A4, A5, A11
.= the EGlobal of V . (f1 . (the_argument_of H)) by A2, A3, A4, A12, Lm25 ;
hence f1 . H = f2 . H by A3, A5, A11; :: thesis: verum

end;

suppose A13: H is conjunctive ; :: thesis: f1 . H = f2 . H

then len (the_left_argument_of H) < len H by Lm23;
then len (the_left_argument_of H) <= k by A5, Lm1;
then A14: f1 . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A2, A3, A4, Lm25;
len (the_right_argument_of H) < len H by A13, Lm23;
then A15: len (the_right_argument_of H) <= k by A5, Lm1;
f2 . H = the L_meet of V . ((f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H))) by A4, A5, A13
.= the L_meet of V . ((f1 . (the_left_argument_of H)),(f1 . (the_right_argument_of H))) by A2, A3, A4, A14, A15, Lm25 ;
hence f1 . H = f2 . H by A3, A5, A13; :: thesis: verum

end;

suppose A16: H is ExistUntill ; :: thesis: f1 . H = f2 . H

then len (the_left_argument_of H) < len H by Lm23;
then len (the_left_argument_of H) <= k by A5, Lm1;
then A17: f1 . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A2, A3, A4, Lm25;
len (the_right_argument_of H) < len H by A16, Lm23;
then A18: len (the_right_argument_of H) <= k by A5, Lm1;
f2 . H = the EUntill of V . ((f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H))) by A4, A5, A16
.= the EUntill of V . ((f1 . (the_left_argument_of H)),(f1 . (the_right_argument_of H))) by A2, A3, A4, A17, A18, Lm25 ;
hence f1 . H = f2 . H by A3, A5, A16; :: thesis: verum

end;

end;

end;

A19: S₁[ 0 ] by Lm10;
for n being Nat holds S₁[n] from NAT_1:sch 2(A19, A1);
hence ( f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai implies for H being CTL-formula st len H <= n holds
f1 . H = f2 . H ) ; :: thesis: verum