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 f, g being Assign of (BASSModel R,BASSIGN) holds
( s |= f EU g 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 |= f ) & pai . m |= g ) ) )
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 f, g being Assign of (BASSModel R,BASSIGN) holds
( s |= f EU g 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 |= f ) & pai . m |= g ) ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel R,BASSIGN) holds
( s |= f EU g 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 |= f ) & pai . m |= g ) ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (BASSModel R,BASSIGN) holds
( s |= f EU g 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 |= f ) & pai . m |= g ) ) )
let f, g be Assign of (BASSModel R,BASSIGN); :: thesis: ( s |= f EU g 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 |= f ) & pai . m |= g ) ) )
A1: f EU g = EUntill_0 f,g,R by Def54;
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 |= f ) & pai . m |= g ) ) implies s |= f EU g )

proof

assume A3: 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 |= f ) & pai . m |= g ) ) ; :: thesis: s |= f EU g
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
(Fid f,S) . (pai . j) = TRUE ) & (Fid g,S) . (pai . m) = TRUE ) )

proof

consider pai being inf_path of R such that
A4: pai . 0 = s and
A5: ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g ) by A3;
take pai ; :: thesis: ( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
(Fid f,S) . (pai . j) = TRUE ) & (Fid g,S) . (pai . m) = TRUE ) )
ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
(Fid f,S) . (pai . j) = TRUE ) & (Fid g,S) . (pai . m) = TRUE )

proof

consider m being Element of NAT such that
A6: for j being Element of NAT st j < m holds
pai . j |= f and
A7: pai . m |= g by A5;
take m ; :: thesis: ( ( for j being Element of NAT st j < m holds
(Fid f,S) . (pai . j) = TRUE ) & (Fid g,S) . (pai . m) = TRUE )
for j being Element of NAT st j < m holds
(Fid f,S) . (pai . j) = TRUE

proof

let j be Element of NAT ; :: thesis: ( j < m implies (Fid f,S) . (pai . j) = TRUE )
assume j < m ; :: thesis: (Fid f,S) . (pai . j) = TRUE
then pai . j |= f by A6;
hence (Fid f,S) . (pai . j) = TRUE by Def59; :: thesis: verum

end;

hence ( ( for j being Element of NAT st j < m holds
(Fid f,S) . (pai . j) = TRUE ) & (Fid g,S) . (pai . m) = TRUE ) by A7, Def59; :: thesis: verum

end;

hence ( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
(Fid f,S) . (pai . j) = TRUE ) & (Fid g,S) . (pai . m) = TRUE ) ) by A4; :: thesis: verum

end;

then EUntill_univ s,(Fid f,S),(Fid g,S),R = TRUE by Def52;
then (Fid (f EU g),S) . s = TRUE by A1, Def53;
hence s |= f EU g by Def59; :: thesis: verum

end;

( s |= f EU g 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 |= f ) & pai . m |= g ) ) )

proof

assume s |= f EU g ; :: 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 |= f ) & pai . m |= g ) )
then (Fid (EUntill_0 f,g,R),S) . s = TRUE by A1, Def59;
then EUntill_univ s,(Fid f,S),(Fid g,S),R = TRUE by Def53;
then consider 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
(Fid f,S) . (pai . j) = TRUE ) & (Fid g,S) . (pai . m) = TRUE ) by Def52;
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 |= f ) & pai . m |= g ) )
ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g )

proof

consider m being Element of NAT such that
A10: for j being Element of NAT st j < m holds
(Fid f,S) . (pai . j) = TRUE and
A11: (Fid g,S) . (pai . m) = TRUE by A9;
take m ; :: thesis: ( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g )
for j being Element of NAT st j < m holds
pai . j |= f

proof

let j be Element of NAT ; :: thesis: ( j < m implies pai . j |= f )
assume j < m ; :: thesis: pai . j |= f
then (Fid f,S) . (pai . j) = TRUE by A10;
hence pai . j |= f by Def59; :: thesis: verum

end;

hence ( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g ) by A11, Def59; :: 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 |= f ) & pai . m |= g ) ) by A8; :: thesis: verum

end;

hence ( s |= f EU g 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 |= f ) & pai . m |= g ) ) ) by A2; :: thesis: verum