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 (BASSModel (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 (BASSModel (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 (BASSModel (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 (BASSModel (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 |= Foax (g,f,(f EU g)) implies s |= f EU g )

proof

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

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

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

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

end;

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

set h = f EU g;
s |= EX (f EU g) by A5, Th13;
then consider pai being inf_path of R such that
A6: pai . 0 = s and
A7: pai . 1 |= f EU g by Th14;
consider pai1 being inf_path of R such that
A8: pai1 . 0 = pai . 1 and
A9: ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai1 . j |= f ) & pai1 . m |= g ) by A7, Th16;
set PAI = PathConc (pai,pai1,1);
reconsider PAI = PathConc (pai,pai1,1) as inf_path of R by A8, Th38;
A10: PAI . 0 = PathChange (pai,pai1,1,0) by Def69
.= s by A6, Def68 ;
consider m being Element of NAT such that
A11: for j being Element of NAT st j < m holds
pai1 . j |= f and
A12: pai1 . m |= g by A9;
set m1 = m + 1;
A13: not m + 1 < 1 by NAT_1:11;
A14: s |= f by A5, Th13;
A15: 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 A16: 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 A14, A10, NAT_1:14; :: thesis: verum

end;

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

set k0 = k - 1;
reconsider k0 = k - 1 as Element of NAT by A17, NAT_1:21;
(k - 1) + 1 <= m by A16, INT_1:7;
then A18: k0 < m by NAT_1:13;
PAI . k = PathChange (pai,pai1,1,k) by Def69
.= pai1 . k0 by A17, Def68 ;
hence PAI . k |= f by A11, A18; :: thesis: verum

end;

end;

end;

PAI . (m + 1) = PathChange (pai,pai1,1,(m + 1)) by Def69
.= pai1 . ((m + 1) - 1) by A13, Def68
.= pai1 . m ;
hence s |= f EU g by A12, A10, A15, Th16; :: thesis: verum

end;

end;

end;

( 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
A19: pai . 0 = s and
A20: 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
A21: for j being Element of NAT st j < m holds
pai . j |= f and
A22: pai . m |= g by A20;

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 A19, A22, Th17; :: thesis: verum

end;

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

set k = m - 1;
reconsider k = m - 1 as Element of NAT by A23, NAT_1:20;
set h = f EU g;
set pai1 = PathShift (pai,1);
A24: (PathShift (pai,1)) . k = pai . (k + 1) by Def67
.= pai . m ;
A25: 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 j < k ; :: thesis: (PathShift (pai,1)) . j |= f
then j + 1 <= k by INT_1:7;
then j + 1 < k + 1 by NAT_1:13;
then pai . (j + 1) |= f by A21;
hence (PathShift (pai,1)) . j |= f by Def67; :: thesis: verum

end;

(PathShift (pai,1)) . 0 = pai . (0 + 1) by Def67
.= pai . 1 ;
then pai . 1 |= f EU g by A22, A24, A25, Th16;
then A26: s |= EX (f EU g) by A19, Th14;
s |= f by A19, A21, A23;
then s |= Fax (f,(f EU g)) by A26, Th13;
hence s |= Foax (g,f,(f EU g)) by Th17; :: thesis: verum

end;

end;

end;

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