let n be Nat; :: thesis: for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for f1, f2 being Function of LTL_WFF, the carrier of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being LTL-formula st len H <= n holds
f1 . H = f2 . H
let V be LTLModel; :: thesis: for Kai being Function of atomic_LTL, the BasicAssign of V
for f1, f2 being Function of LTL_WFF, the carrier of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being LTL-formula st len H <= n holds
f1 . H = f2 . H
let Kai be Function of atomic_LTL, the BasicAssign of V; :: thesis: for f1, f2 being Function of LTL_WFF, the carrier of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being LTL-formula st len H <= n holds
f1 . H = f2 . H
let f1, f2 be Function of LTL_WFF, the carrier of V; :: thesis: ( f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai implies for H being LTL-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 LTL-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 LTL-formula st len H <= k + 1 holds
f1 . H = f2 . H
let H be LTL-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 next or H is conjunctive or H is disjunctive or H is Until or H is Release ) 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 Th10;
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, Lm23 ;
hence f1 . H = f2 . H by A3, A5, A7; :: thesis: verum

end;

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

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

end;

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

then len (the_left_argument_of H) < len H by Th11;
then len (the_left_argument_of H) <= k by A5, Lm1;
then A12: f1 . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A2, A3, A4, Lm23;
len (the_right_argument_of H) < len H by A11, Th11;
then A13: 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, A11
.= the L_meet of V . ((f1 . (the_left_argument_of H)),(f1 . (the_right_argument_of H))) by A2, A3, A4, A12, A13, Lm23 ;
hence f1 . H = f2 . H by A3, A5, A11; :: thesis: verum

end;

suppose A14: H is disjunctive ; :: thesis: f1 . H = f2 . H

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

end;

suppose A17: H is Until ; :: thesis: f1 . H = f2 . H

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

end;

suppose A20: H is Release ; :: thesis: f1 . H = f2 . H

then len (the_left_argument_of H) < len H by Th11;
then len (the_left_argument_of H) <= k by A5, Lm1;
then A21: f1 . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A2, A3, A4, Lm23;
len (the_right_argument_of H) < len H by A20, Th11;
then A22: len (the_right_argument_of H) <= k by A5, Lm1;
f2 . H = the RELEASE of V . ((f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H))) by A4, A5, A20
.= the RELEASE of V . ((f1 . (the_left_argument_of H)),(f1 . (the_right_argument_of H))) by A2, A3, A4, A21, A22, Lm23 ;
hence f1 . H = f2 . H by A3, A5, A20; :: thesis: verum

end;

end;

end;

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