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 )

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

assume A1: F \/ {A} |= B ; :: thesis: F |= ('G' A) => B
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

proof

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

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

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;

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

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

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;

then A5: M ^\ n |= {A} by Th23, Def12;
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;

end;

end;

end;

end;

assume A7: F |= ('G' A) => B ; :: thesis: F \/ {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