let H be CTL-formula; 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; 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; 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))
; verum