let A, B be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |=0 'G' A & F |=0 'G' (A => B) holds

F |=0 'G' B

let F be Subset of LTLB_WFF; :: thesis: ( F |=0 'G' A & F |=0 'G' (A => B) implies F |=0 'G' B )

assume that

A1: F |=0 'G' A and

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

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

assume B10: M |=0 F ; :: thesis: M |=0 'G' B

then B11: M |=0 'G' A by A1;

B12: M |=0 'G' (A => B) by B10, A2;

F |=0 'G' B

let F be Subset of LTLB_WFF; :: thesis: ( F |=0 'G' A & F |=0 'G' (A => B) implies F |=0 'G' B )

assume that

A1: F |=0 'G' A and

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

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

assume B10: M |=0 F ; :: thesis: M |=0 'G' B

then B11: M |=0 'G' A by A1;

B12: M |=0 'G' (A => B) by B10, A2;

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

hence
M |=0 'G' B
by LTLAXIO1:10; :: thesis: verumlet i be Element of NAT ; :: thesis: (SAT M) . [(0 + i),B] = 1

B13: (SAT M) . [(0 + i),A] = 1 by B11, LTLAXIO1:10;

(SAT M) . [(0 + i),(A => B)] = 1 by B12, LTLAXIO1:10;

then ((SAT M) . [i,A]) => ((SAT M) . [i,B]) = 1 by LTLAXIO1:def 11;

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

end;B13: (SAT M) . [(0 + i),A] = 1 by B11, LTLAXIO1:10;

(SAT M) . [(0 + i),(A => B)] = 1 by B12, LTLAXIO1:10;

then ((SAT M) . [i,A]) => ((SAT M) . [i,B]) = 1 by LTLAXIO1:def 11;

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