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)

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

defpred S_{1}[ Nat] means (SAT M) . [(n + $1),A] = 1;

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)

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

defpred S

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

end;

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

A5:
for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A4;

A8: for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A7, A5);

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

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

end;S

proof

A7:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

(SAT M) . [(n + kk),(A => ('X' A))] = 1 by A2, A3, Def12;

then ((SAT M) . [(n + kk),A]) => ((SAT M) . [(n + kk),('X' A)]) = 1 by Def11;

then (SAT M) . [((n + kk) + 1),A] = 1 by A6, Th9;

hence S_{1}[k + 1]
; :: thesis: verum

end;assume A6: S

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

(SAT M) . [(n + kk),(A => ('X' A))] = 1 by A2, A3, Def12;

then ((SAT M) . [(n + kk),A]) => ((SAT M) . [(n + kk),('X' A)]) = 1 by Def11;

then (SAT M) . [((n + kk) + 1),A] = 1 by A6, Th9;

hence S

A8: for i being Nat holds S

now :: thesis: for i being Element of NAT holds (SAT M) . [(n + i),B] = 1

then
(SAT M) . [n,('G' B)] = 1
by Th10;let i be Element of NAT ; :: thesis: (SAT M) . [(n + i),B] = 1

(SAT M) . [(n + i),(A => B)] = 1 by A3, A1, Def12;

then A9: ((SAT M) . [(n + i),A]) => ((SAT M) . [(n + i),B]) = 1 by Def11;

(SAT M) . [(n + i),A] = 1 by A8;

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

end;(SAT M) . [(n + i),(A => B)] = 1 by A3, A1, Def12;

then A9: ((SAT M) . [(n + i),A]) => ((SAT M) . [(n + i),B]) = 1 by Def11;

(SAT M) . [(n + i),A] = 1 by A8;

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

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

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