let H be LTL-formula; for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate (('X' H),Kai) = 'X' (Evaluate (H,Kai))
let V be LTLModel; 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; Evaluate (('X' H),Kai) = 'X' (Evaluate (H,Kai))
consider f1 being Function of LTL_WFF, the carrier of V such that
A1:
f1 is-Evaluation-for Kai
and
A2:
Evaluate (('X' H),Kai) = f1 . ('X' H)
by Def35;
A3:
ex f2 being Function of LTL_WFF, the carrier of V st
( f2 is-Evaluation-for Kai & Evaluate (H,Kai) = f2 . H )
by Def35;
A4:
'X' H is next
;
then A5:
not 'X' H is negative
by Lm19;
Evaluate (('X' H),Kai) =
the NEXT of V . (f1 . (the_argument_of ('X' H)))
by A1, A2, A4
.=
the NEXT of V . (f1 . H)
by A4, A5, Def18
.=
'X' (Evaluate (H,Kai))
by A1, A3, Th49
;
hence
Evaluate (('X' H),Kai) = 'X' (Evaluate (H,Kai))
; verum