let H1, H2 be LTL-formula; :: thesis: for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V holds Evaluate (H1 'R' H2),Kai = (Evaluate H1,Kai) 'R' (Evaluate H2,Kai)
let V be LTLModelStr ; :: thesis: for Kai being Function of atomic_LTL ,the BasicAssign of V holds Evaluate (H1 'R' H2),Kai = (Evaluate H1,Kai) 'R' (Evaluate H2,Kai)
let Kai be Function of atomic_LTL ,the BasicAssign of V; :: thesis: Evaluate (H1 'R' H2),Kai = (Evaluate H1,Kai) 'R' (Evaluate H2,Kai)
consider f0 being Function of LTL_WFF ,the Assignations of V such that
A1: f0 is-Evaluation-for Kai and
A2: Evaluate (H1 'R' H2),Kai = f0 . (H1 'R' H2) by Def32;
consider f1 being Function of LTL_WFF ,the Assignations of V such that
A3: f1 is-Evaluation-for Kai and
A4: Evaluate H1,Kai = f1 . H1 by Def32;
consider f2 being Function of LTL_WFF ,the Assignations of V such that
A5: f2 is-Evaluation-for Kai and
A6: Evaluate H2,Kai = f2 . H2 by Def32;
A7: ( f0 = f1 & f0 = f2 ) by A1, A3, A5, Th4;
A8: H1 'R' H2 is Release by Def1901;
then ( not H1 'R' H2 is conjunctive & not H1 'R' H2 is disjunctive & not H1 'R' H2 is Until ) by Lm1801;
then ( the_left_argument_of (H1 'R' H2) = H1 & the_right_argument_of (H1 'R' H2) = H2 ) by A8, Def22, Def23;
hence Evaluate (H1 'R' H2),Kai = (Evaluate H1,Kai) 'R' (Evaluate H2,Kai) by A1, A2, A7, A8, Def26, A4, A6; :: thesis: verum