let S be non empty set ; :: thesis: for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN)
for s being Element of S holds
( s |= f EU g iff s |= Foax g,f,(f EU g) )
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN)
for s being Element of S holds
( s |= f EU g iff s |= Foax g,f,(f EU g) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (CTLModel R,BASSIGN)
for s being Element of S holds
( s |= f EU g iff s |= Foax g,f,(f EU g) )
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: for s being Element of S holds
( s |= f EU g iff s |= Foax g,f,(f EU g) )
let s be Element of S; :: thesis: ( s |= f EU g iff s |= Foax g,f,(f EU g) )
A1: ( s |= f EU g implies s |= Foax g,f,(f EU g) )

proof

assume s |= f EU g ; :: thesis: s |= Foax g,f,(f EU g)
then consider 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 |= f ) & pai . m |= g ) by Th16;
consider m being Element of NAT such that
A4: for j being Element of NAT st j < m holds
pai . j |= f and
A5: pai . m |= g by A3;

per cases ( m = 0 or m > 0 ) ;

suppose m = 0 ; :: thesis: s |= Foax g,f,(f EU g)

hence s |= Foax g,f,(f EU g) by A2, A5, Th17; :: thesis: verum

end;

suppose A6: m > 0 ; :: thesis: s |= Foax g,f,(f EU g)

set h = f EU g;
set k = m - 1;
reconsider k = m - 1 as Element of NAT by A6, NAT_1:20;
A7: s |= f by A2, A4, A6;
set pai1 = PathShift pai,1;
A8: (PathShift pai,1) . 0 = pai . (0 + 1) by Def67
.= pai . 1 ;
A9: (PathShift pai,1) . k = pai . (k + 1) by Def67
.= pai . m ;
for j being Element of NAT st j < k holds
(PathShift pai,1) . j |= f

proof

let j be Element of NAT ; :: thesis: ( j < k implies (PathShift pai,1) . j |= f )
assume A10: j < k ; :: thesis: (PathShift pai,1) . j |= f
set j1 = j + 1;
j + 1 < m

proof

j + 1 <= k by A10, INT_1:20;
then j + 1 < k + 1 by NAT_1:13;
hence j + 1 < m ; :: thesis: verum

end;

then pai . (j + 1) |= f by A4;
hence (PathShift pai,1) . j |= f by Def67; :: thesis: verum

end;

then pai . 1 |= f EU g by A5, A8, A9, Th16;
then s |= EX (f EU g) by A2, Th14;
then s |= Fax f,(f EU g) by A7, Th13;
hence s |= Foax g,f,(f EU g) by Th17; :: thesis: verum

end;

end;

end;

( s |= Foax g,f,(f EU g) implies s |= f EU g )

proof

assume A11: s |= Foax g,f,(f EU g) ; :: thesis: s |= f EU g

per cases ( s |= g or s |= Fax f,(f EU g) ) by A11, Th17;

suppose A12: s |= g ; :: thesis: s |= f EU g

consider pai being inf_path of R such that
A13: pai . 0 = s by Th25;
set m = 0 ;
for j being Element of NAT st j < 0 holds
pai . j |= f ;
hence s |= f EU g by A12, A13, Th16; :: thesis: verum

end;

suppose A14: s |= Fax f,(f EU g) ; :: thesis: s |= f EU g

set h = f EU g;
A15: ( s |= f & s |= EX (f EU g) ) by A14, Th13;
then consider pai being inf_path of R such that
A16: pai . 0 = s and
A17: pai . 1 |= f EU g by Th14;
consider pai1 being inf_path of R such that
A18: pai1 . 0 = pai . 1 and
A19: ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai1 . j |= f ) & pai1 . m |= g ) by A17, Th16;
consider m being Element of NAT such that
A20: for j being Element of NAT st j < m holds
pai1 . j |= f and
A21: pai1 . m |= g by A19;
set PAI = PathConc pai,pai1,1;
reconsider PAI = PathConc pai,pai1,1 as inf_path of R by A18, Th38;
set m1 = m + 1;
A22: PAI . 0 = PathChange pai,pai1,1,0 by Def69
.= s by A16, Def68 ;
A23: not m + 1 < 1 by NAT_1:11;
A24: PAI . (m + 1) = PathChange pai,pai1,1,(m + 1) by Def69
.= pai1 . ((m + 1) - 1) by A23, Def68
.= pai1 . m ;
for k being Element of NAT st k < m + 1 holds
PAI . k |= f

proof

let k be Element of NAT ; :: thesis: ( k < m + 1 implies PAI . k |= f )
assume A25: k < m + 1 ; :: thesis: PAI . k |= f

per cases ( k < 1 or not k < 1 ) ;

suppose k < 1 ; :: thesis: PAI . k |= f

hence PAI . k |= f by A15, A22, NAT_1:14; :: thesis: verum

end;

suppose A26: not k < 1 ; :: thesis: PAI . k |= f

set k0 = k - 1;
reconsider k0 = k - 1 as Element of NAT by A26, NAT_1:21;
A27: PAI . k = PathChange pai,pai1,1,k by Def69
.= pai1 . k0 by A26, Def68 ;
k0 < m

proof

(k - 1) + 1 <= m by A25, INT_1:20;
hence k0 < m by NAT_1:13; :: thesis: verum

end;

hence PAI . k |= f by A20, A27; :: thesis: verum

end;

end;

end;

hence s |= f EU g by A21, A22, A24, Th16; :: thesis: verum

end;

end;

end;

hence ( s |= f EU g iff s |= Foax g,f,(f EU g) ) by A1; :: thesis: verum