let H be LTL-formula; :: thesis: for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai))
let V be LTLModel; :: thesis: for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai))
let Kai be Function of atomic_LTL, the BasicAssign of V; :: thesis: Evaluate (('not' H),Kai) = 'not' (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 (('not' H),Kai) = f1 . ('not' 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: 'not' H is negative ;
then Evaluate (('not' H),Kai) = the Compl of V . (f1 . (the_argument_of ('not' H))) by A1, A2
.= the Compl of V . (f1 . H) by A4, Def18
.= 'not' (Evaluate (H,Kai)) by A1, A3, Th49 ;
hence Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai)) ; :: thesis: verum