let H1, H2 be CTL-formula; :: thesis: for V being CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V holds Evaluate (H1 'or' H2),Kai = (Evaluate H1,Kai) 'or' (Evaluate H2,Kai)
let V be CTLModelStr ; :: thesis: for Kai being Function of atomic_WFF ,the BasicAssign of V holds Evaluate (H1 'or' H2),Kai = (Evaluate H1,Kai) 'or' (Evaluate H2,Kai)
let Kai be Function of atomic_WFF ,the BasicAssign of V; :: thesis: Evaluate (H1 'or' H2),Kai = (Evaluate H1,Kai) 'or' (Evaluate H2,Kai)
Evaluate (H1 'or' H2),Kai = 'not' (Evaluate (('not' H1) '&' ('not' H2)),Kai) by Th5
.= 'not' ((Evaluate ('not' H1),Kai) '&' (Evaluate ('not' H2),Kai)) by Th6
.= 'not' (('not' (Evaluate H1,Kai)) '&' (Evaluate ('not' H2),Kai)) by Th5 ;
hence Evaluate (H1 'or' H2),Kai = (Evaluate H1,Kai) 'or' (Evaluate H2,Kai) by Th5; :: thesis: verum