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 being Assign of (BASSModel (R,BASSIGN))
for s being Element of S holds
( s |= EG f iff s |= Fax (f,(EG f)) )
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN))
for s being Element of S holds
( s |= EG f iff s |= Fax (f,(EG f)) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (BASSModel (R,BASSIGN))
for s being Element of S holds
( s |= EG f iff s |= Fax (f,(EG f)) )
let f be Assign of (BASSModel (R,BASSIGN)); :: thesis: for s being Element of S holds
( s |= EG f iff s |= Fax (f,(EG f)) )
let s be Element of S; :: thesis: ( s |= EG f iff s |= Fax (f,(EG f)) )
set g = EG f;
thus ( s |= EG f implies s |= Fax (f,(EG f)) ) :: thesis: ( s |= Fax (f,(EG f)) implies s |= EG f )

proof

set g = EG f;
assume s |= EG f ; :: thesis: s |= Fax (f,(EG f))
then consider pai being inf_path of R such that
A1: pai . 0 = s and
A2: for n being Element of NAT holds pai . n |= f by Th15;
set pai1 = PathShift (pai,1);
A3: for n being Element of NAT holds (PathShift (pai,1)) . n |= f

proof

let n be Element of NAT ; :: thesis: (PathShift (pai,1)) . n |= f
set n1 = n + 1;
(PathShift (pai,1)) . n = pai . (n + 1) by Def67;
hence (PathShift (pai,1)) . n |= f by A2; :: thesis: verum

end;

pai . (0 + 1) = (PathShift (pai,1)) . 0 by Def67;
then pai . 1 |= EG f by A3, Th15;
then A4: s |= EX (EG f) by A1, Th14;
s |= f by A1, A2;
hence s |= Fax (f,(EG f)) by A4, Th13; :: thesis: verum

end;

assume A5: s |= Fax (f,(EG f)) ; :: thesis: s |= EG f
then s |= EX (EG f) by Th13;
then consider pai1 being inf_path of R such that
A6: pai1 . 0 = s and
A7: pai1 . 1 |= EG f by Th14;
consider pai2 being inf_path of R such that
A8: pai2 . 0 = pai1 . 1 and
A9: for n being Element of NAT holds pai2 . n |= f by A7, Th15;
set pai = PathConc (pai1,pai2,1);
reconsider pai = PathConc (pai1,pai2,1) as inf_path of R by A8, Th38;
A10: pai . 0 = PathChange (pai1,pai2,1,0) by Def69
.= s by A6, Def68 ;
for n being Element of NAT holds pai . n |= f

proof

let n be Element of NAT ; :: thesis: pai . n |= f

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

suppose A11: n < 1 ; :: thesis: pai . n |= f

n = 0

proof

assume A12: n <> 0 ; :: thesis: contradiction
n < 0 + 1 by A11;
hence contradiction by A12, NAT_1:22; :: thesis: verum

end;

hence pai . n |= f by A5, A10, Th13; :: thesis: verum

end;

suppose A13: not n < 1 ; :: thesis: pai . n |= f

then reconsider m = n - 1 as Element of NAT by NAT_1:21;
pai . n = PathChange (pai1,pai2,1,n) by Def69
.= pai2 . m by A13, Def68 ;
hence pai . n |= f by A9; :: thesis: verum

end;

end;

end;

hence s |= EG f by A10, Th15; :: thesis: verum