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 ) ) )
( s,kai |= H1 EU H2 iff s |= Evaluate (H1 EU H2),kai ) by Def60;
then A1: ( s,kai |= H1 EU H2 iff s |= (Evaluate H1,kai) EU (Evaluate H2,kai) ) by Th9;
A2: ( 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 A3: ( 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 ) ) ; :: 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 ) & pai . m |= Evaluate H2,kai ) by A3;
A5: ( pai . m |= Evaluate H2,kai iff pai . m,kai |= H2 ) by Def60;
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 A6: j < m ; :: thesis: pai . j,kai |= H1
pai . j |= Evaluate H1,kai by A4, A6;
hence pai . j,kai |= H1 by Def60; :: thesis: verum

end;

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 A3, A4, A5; :: thesis: verum

end;

( 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 A7: ( 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 ) ) ; :: 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
A8: ( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) by A7;
A9: ( pai . m |= Evaluate H2,kai iff pai . m,kai |= H2 ) by Def60;
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 A10: j < m ; :: thesis: pai . j |= Evaluate H1,kai
pai . j,kai |= H1 by A8, A10;
hence pai . j |= Evaluate H1,kai by Def60; :: thesis: verum

end;

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 A7, A8, A9; :: thesis: verum

end;

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, A2, Th16; :: thesis: verum