let A, B be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |= A => B & F |= A => ('X' A) holds
F |= A => ('G' B)
let F be Subset of LTLB_WFF; :: thesis: ( F |= A => B & F |= A => ('X' A) implies F |= A => ('G' B) )
assume that
A1: F |= A => B and
A2: F |= A => ('X' A) ; :: thesis: F |= A => ('G' B)
let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F implies M |= A => ('G' B) )
assume A3: M |= F ; :: thesis: M |= A => ('G' B)
then A4: M |= A => B by A1, Def15;
A5: M |= A => ('X' A) by A2, A3, Def15;
let n be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [n,(A => ('G' B))] = 1
defpred S₁[ Nat] means (SAT M) . [(n + $1),A] = 1;

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

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

A7: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
(SAT M) . [(n + k),(A => ('X' A))] = 1 by A5, Def13;
then ((SAT M) . [(n + k),A]) => ((SAT M) . [(n + k),('X' A)]) = 1 by Def12;
then (SAT M) . [((n + k) + 1),A] = 1 by A8, Th10;
hence S₁[k + 1] ; :: thesis: verum

end;

A9: S₁[ 0 ] by A6;
A10: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A9, A7);

now

let i be Element of NAT ; :: thesis: (SAT M) . [(n + i),B] = 1
(SAT M) . [(n + i),(A => B)] = 1 by A4, Def13;
then A11: ((SAT M) . [(n + i),A]) => ((SAT M) . [(n + i),B]) = 1 by Def12;
(SAT M) . [(n + i),A] = 1 by A10;
hence (SAT M) . [(n + i),B] = 1 by A11; :: thesis: verum

end;

then (SAT M) . [n,('G' B)] = 1 by Th11;
then ((SAT M) . [n,A]) => ((SAT M) . [n,('G' B)]) = 1 ;
hence (SAT M) . [n,(A => ('G' B))] = 1 by Def12; :: thesis: verum

end;

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

then ((SAT M) . [n,A]) => ((SAT M) . [n,('G' B)]) = 1 ;
hence (SAT M) . [n,(A => ('G' B))] = 1 by Def12; :: thesis: verum

end;

end;