let H1, H2 be CTL-formula; for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 EU H2),Kai) = (Evaluate (H1,Kai)) EU (Evaluate (H2,Kai))
let V be CTLModel; for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 EU H2),Kai) = (Evaluate (H1,Kai)) EU (Evaluate (H2,Kai))
let Kai be Function of atomic_WFF, the BasicAssign of V; Evaluate ((H1 EU H2),Kai) = (Evaluate (H1,Kai)) EU (Evaluate (H2,Kai))
consider f0 being Function of CTL_WFF, the carrier of V such that
A1:
f0 is-Evaluation-for Kai
and
A2:
Evaluate ((H1 EU H2),Kai) = f0 . (H1 EU H2)
by Def34;
consider f1 being Function of CTL_WFF, the carrier of V such that
A3:
f1 is-Evaluation-for Kai
and
A4:
Evaluate (H1,Kai) = f1 . H1
by Def34;
consider f2 being Function of CTL_WFF, the carrier of V such that
A5:
f2 is-Evaluation-for Kai
and
A6:
Evaluate (H2,Kai) = f2 . H2
by Def34;
A7:
f0 = f2
by A1, A5, Th4;
A8:
H1 EU H2 is ExistUntill
;
then
(H1 EU H2) . 1 = 4
by Lm7;
then A9:
not H1 EU H2 is conjunctive
by Lm4;
then A10:
the_left_argument_of (H1 EU H2) = H1
by A8, Def22;
A11:
the_right_argument_of (H1 EU H2) = H2
by A8, A9, Def23;
f0 = f1
by A1, A3, Th4;
hence
Evaluate ((H1 EU H2),Kai) = (Evaluate (H1,Kai)) EU (Evaluate (H2,Kai))
by A1, A2, A4, A6, A7, A8, A10, A11; verum