let H1, H2 be CTL-formula; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum