let H1, H2 be CTL-formula; :: thesis: for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let S be non empty set ; :: thesis: for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let R be total Relation of S,S; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)); :: thesis: ( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
A1: ( ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) ) implies ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )

proof

given pai being inf_path of R such that A2: pai . 0 = s and
A3: ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) )
take pai ; :: thesis: ( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) )
consider m being Element of NAT such that
A4: for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) and
A5: pai . m |= Evaluate (H2,kai) by A3;
A6: for j being Element of NAT st j < m holds
pai . j,kai |= H1 by A4;
( pai . m |= Evaluate (H2,kai) iff pai . m,kai |= H2 ) ;
hence ( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) by A2, A5, A6; :: thesis: verum

end;

A7: ( ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) implies ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) ) )

proof

given pai being inf_path of R such that A8: pai . 0 = s and
A9: ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) )
take pai ; :: thesis: ( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) )
consider m being Element of NAT such that
A10: for j being Element of NAT st j < m holds
pai . j,kai |= H1 and
A11: pai . m,kai |= H2 by A9;
A12: for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) by A10, Def60;
thus ( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) ) by A8, A11, A12; :: thesis: verum

end;

( s,kai |= H1 EU H2 iff s |= (Evaluate (H1,kai)) EU (Evaluate (H2,kai)) ) by Th9;
hence ( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) ) by A1, A7, Th16; :: thesis: verum