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

( F \/ {A} |= B iff F |= ('G' A) => B )

let F be Subset of LTLB_WFF; :: thesis: ( F \/ {A} |= B iff F |= ('G' A) => B )

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F \/ {A} implies M |= B )

assume A8: M |= F \/ {A} ; :: thesis: M |= B

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

M |= {A} by A8, Th22;

then for j being Element of NAT holds (SAT M) . [(i + j),A] = 1 by Def12, Th23;

then A9: (SAT M) . [i,('G' A)] = 1 by Th10;

M |= F by A8, Th22;

then (SAT M) . [i,(('G' A) => B)] = 1 by Def12, A7;

then ((SAT M) . [i,('G' A)]) => ((SAT M) . [i,B]) = 1 by Def11;

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

( F \/ {A} |= B iff F |= ('G' A) => B )

let F be Subset of LTLB_WFF; :: thesis: ( F \/ {A} |= B iff F |= ('G' A) => B )

hereby :: thesis: ( F |= ('G' A) => B implies F \/ {A} |= B )

assume A7:
F |= ('G' A) => B
; :: thesis: F \/ {A} |= Bassume A1:
F \/ {A} |= B
; :: thesis: F |= ('G' A) => B

thus F |= ('G' A) => B :: thesis: verum

end;thus F |= ('G' A) => B :: thesis: verum

proof

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F implies M |= ('G' A) => B )

assume A2: M |= F ; :: thesis: M |= ('G' A) => B

thus M |= ('G' A) => B :: thesis: verum

end;assume A2: M |= F ; :: thesis: M |= ('G' A) => B

thus M |= ('G' A) => B :: thesis: verum

proof

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

end;per cases
( (SAT M) . [n,('G' A)] = 0 or (SAT M) . [n,('G' A)] = 1 )
by XBOOLEAN:def 3;

end;

suppose A3:
(SAT M) . [n,('G' A)] = 0
; :: thesis: (SAT M) . [n,(('G' A) => B)] = 1

thus (SAT M) . [n,(('G' A) => B)] =
((SAT M) . [n,('G' A)]) => ((SAT M) . [n,B])
by Def11

.= 1 by A3 ; :: thesis: verum

end;.= 1 by A3 ; :: thesis: verum

suppose A4:
(SAT M) . [n,('G' A)] = 1
; :: thesis: (SAT M) . [n,(('G' A) => B)] = 1

M ^\ n |= F by A2, Th29;

then M ^\ n |= F \/ {A} by A5, Th22;

then (SAT (M ^\ n)) . [0,B] = 1 by Def12, A1;

then A6: (SAT M) . [(n + 0),B] = 1 by Th28;

thus (SAT M) . [n,(('G' A) => B)] = ((SAT M) . [n,('G' A)]) => ((SAT M) . [n,B]) by Def11

.= 1 by A6 ; :: thesis: verum

end;

now :: thesis: for j being Element of NAT holds (SAT (M ^\ n)) . [j,A] = 1

then A5:
M ^\ n |= {A}
by Th23, Def12;let j be Element of NAT ; :: thesis: (SAT (M ^\ n)) . [j,A] = 1

(SAT M) . [(n + j),A] = 1 by A4, Th10;

hence (SAT (M ^\ n)) . [j,A] = 1 by Th28; :: thesis: verum

end;(SAT M) . [(n + j),A] = 1 by A4, Th10;

hence (SAT (M ^\ n)) . [j,A] = 1 by Th28; :: thesis: verum

M ^\ n |= F by A2, Th29;

then M ^\ n |= F \/ {A} by A5, Th22;

then (SAT (M ^\ n)) . [0,B] = 1 by Def12, A1;

then A6: (SAT M) . [(n + 0),B] = 1 by Th28;

thus (SAT M) . [n,(('G' A) => B)] = ((SAT M) . [n,('G' A)]) => ((SAT M) . [n,B]) by Def11

.= 1 by A6 ; :: thesis: verum

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F \/ {A} implies M |= B )

assume A8: M |= F \/ {A} ; :: thesis: M |= B

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

M |= {A} by A8, Th22;

then for j being Element of NAT holds (SAT M) . [(i + j),A] = 1 by Def12, Th23;

then A9: (SAT M) . [i,('G' A)] = 1 by Th10;

M |= F by A8, Th22;

then (SAT M) . [i,(('G' A) => B)] = 1 by Def12, A7;

then ((SAT M) . [i,('G' A)]) => ((SAT M) . [i,B]) = 1 by Def11;

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