let H be LTL-formula; :: thesis: for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V holds Evaluate ('X' H),Kai = 'X' (Evaluate H,Kai)
let V be LTLModelStr ; :: thesis: for Kai being Function of atomic_LTL ,the BasicAssign of V holds Evaluate ('X' H),Kai = 'X' (Evaluate H,Kai)
let Kai be Function of atomic_LTL ,the BasicAssign of V; :: thesis: Evaluate ('X' H),Kai = 'X' (Evaluate H,Kai)
consider f1 being Function of LTL_WFF ,the Assignations of V such that
A1: f1 is-Evaluation-for Kai and
A2: Evaluate ('X' H),Kai = f1 . ('X' H) by Def32;
consider f2 being Function of LTL_WFF ,the Assignations of V such that
A3: f2 is-Evaluation-for Kai and
A4: Evaluate H,Kai = f2 . H by Def32;
A5: 'X' H is next by Def18;
then A6: not 'X' H is negative by Lm17;
Evaluate ('X' H),Kai = the NEXT of V . (f1 . (the_argument_of ('X' H))) by A2, A1, A5, Def26
.= the NEXT of V . (f1 . H) by A6, A5, Def21
.= 'X' (Evaluate H,Kai) by A1, A3, A4, Th4 ;
hence Evaluate ('X' H),Kai = 'X' (Evaluate H,Kai) ; :: thesis: verum