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 (CTLModel 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 (CTLModel 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 (CTLModel 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 (CTLModel 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 (CTLModel 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 (CTLModel 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

proof

let j be Element of NAT ; :: thesis: ( j < m implies pai . j,kai |= H1 )
assume j < m ; :: thesis: pai . j,kai |= H1
then pai . j |= Evaluate H1,kai by A4;
hence pai . j,kai |= H1 by Def60; :: thesis: verum

end;

( pai . m |= Evaluate H2,kai iff pai . m,kai |= H2 ) by Def60;
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

proof

let j be Element of NAT ; :: thesis: ( j < m implies pai . j |= Evaluate H1,kai )
assume j < m ; :: thesis: pai . j |= Evaluate H1,kai
then pai . j,kai |= H1 by A10;
hence pai . j |= Evaluate H1,kai by Def60; :: thesis: verum

end;

( pai . m |= Evaluate H2,kai iff pai . m,kai |= H2 ) by Def60;
hence ( 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 EU H2),kai ) by Def60;
then ( 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