let H be CTL-formula; :: thesis: for V being CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V holds Evaluate (EX H),Kai = EX (Evaluate H,Kai)
let V be CTLModelStr ; :: thesis: for Kai being Function of atomic_WFF ,the BasicAssign of V holds Evaluate (EX H),Kai = EX (Evaluate H,Kai)
let Kai be Function of atomic_WFF ,the BasicAssign of V; :: thesis: Evaluate (EX H),Kai = EX (Evaluate H,Kai)
consider f1 being Function of CTL_WFF ,the Assignations of V such that
A1: f1 is-Evaluation-for Kai and
A2: Evaluate (EX H),Kai = f1 . (EX H) by Def32;
A3: ex f2 being Function of CTL_WFF ,the Assignations of V st
( f2 is-Evaluation-for Kai & Evaluate H,Kai = f2 . H ) by Def32;
A4: EX H is ExistNext by Def17;
then Evaluate (EX H),Kai = the EneXt of V . (f1 . (the_argument_of (EX H))) by A1, A2, Def26
.= the EneXt of V . (f1 . H) by A4, Def21
.= EX (Evaluate H,Kai) by A1, A3, Th4 ;
hence Evaluate (EX H),Kai = EX (Evaluate H,Kai) ; :: thesis: verum