let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF holds

( F |= A iff 'G' F |=0 A )

let F be Subset of LTLB_WFF; :: thesis: ( F |= A iff 'G' F |=0 A )

thus F |= A :: thesis: verum

( F |= A iff 'G' F |=0 A )

let F be Subset of LTLB_WFF; :: thesis: ( F |= A iff 'G' F |=0 A )

hereby :: thesis: ( 'G' F |=0 A implies F |= A )

assume Z2:
'G' F |=0 A
; :: thesis: F |= Aassume Z1:
F |= A
; :: thesis: 'G' F |=0 A

thus 'G' F |=0 A :: thesis: verum

end;thus 'G' F |=0 A :: thesis: verum

proof

let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 'G' F implies M |=0 A )

assume M |=0 'G' F ; :: thesis: M |=0 A

then M |= A by Z1, th261bq;

hence M |=0 A ; :: thesis: verum

end;assume M |=0 'G' F ; :: thesis: M |=0 A

then M |= A by Z1, th261bq;

hence M |=0 A ; :: thesis: verum

thus F |= A :: thesis: verum

proof

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( not M |= F or M |= A )

assume Z3: M |= F ; :: thesis: M |= A

let i be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [i,A] = 1

M ^\ i |= F by LTLAXIO1:29, Z3;

then M ^\ i |=0 A by Z2, th261bq;

then (SAT M) . [(i + 0),A] = 1 by LTLAXIO1:28;

hence (SAT M) . [i,A] = 1 ; :: thesis: verum

end;assume Z3: M |= F ; :: thesis: M |= A

let i be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [i,A] = 1

M ^\ i |= F by LTLAXIO1:29, Z3;

then M ^\ i |=0 A by Z2, th261bq;

then (SAT M) . [(i + 0),A] = 1 by LTLAXIO1:28;

hence (SAT M) . [i,A] = 1 ; :: thesis: verum