let H be CTL-formula; :: thesis: for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EG H),Kai) = EG (Evaluate (H,Kai))
let V be CTLModel; :: thesis: for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EG H),Kai) = EG (Evaluate (H,Kai))
let Kai be Function of atomic_WFF, the BasicAssign of V; :: thesis: Evaluate ((EG H),Kai) = EG (Evaluate (H,Kai))
consider f1 being Function of CTL_WFF, the carrier of V such that
A1: f1 is-Evaluation-for Kai and
A2: Evaluate ((EG H),Kai) = f1 . (EG H) by Def34;
A3: ex f2 being Function of CTL_WFF, the carrier of V st
( f2 is-Evaluation-for Kai & Evaluate (H,Kai) = f2 . H ) by Def34;
A4: EG H is ExistGlobal ;
then A5: not EG H is negative by Lm18;
A6: not EG H is ExistNext by A4, Lm18;
Evaluate ((EG H),Kai) = the EGlobal of V . (f1 . (the_argument_of (EG H))) by A1, A2, A4
.= the EGlobal of V . (f1 . H) by A4, A5, A6, Def21
.= EG (Evaluate (H,Kai)) by A1, A3, Th4 ;
hence Evaluate ((EG H),Kai) = EG (Evaluate (H,Kai)) ; :: thesis: verum