let B be Element of LTLB_WFF ; :: thesis: for n being Element of NAT

for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1

let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1

let M be LTLModel; :: thesis: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1

A1: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = ((SAT M) . [n,('G' B)]) => ((SAT M) . [n,(B '&&' ('X' ('G' B)))]) by Def11;

for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1

let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1

let M be LTLModel; :: thesis: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1

A1: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = ((SAT M) . [n,('G' B)]) => ((SAT M) . [n,(B '&&' ('X' ('G' B)))]) by Def11;

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

end;

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

end;

end;

suppose A2:
(SAT M) . [n,('G' B)] = 1
; :: thesis: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1

then A3: (SAT M) . [n,('X' ('G' B))] = 1 by Th9;

(SAT M) . [(n + 0),B] = 1 by A2, Th10;

then (SAT M) . [n,(B '&&' ('X' ('G' B)))] = 1 by A3, Th7;

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

end;

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

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

(SAT M) . [(n + (i + 1)),B] = 1 by A2, Th10;

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

end;(SAT M) . [(n + (i + 1)),B] = 1 by A2, Th10;

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

then A3: (SAT M) . [n,('X' ('G' B))] = 1 by Th9;

(SAT M) . [(n + 0),B] = 1 by A2, Th10;

then (SAT M) . [n,(B '&&' ('X' ('G' B)))] = 1 by A3, Th7;

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