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;
per cases ( (SAT M) . [n,('G' B)] = 0 or (SAT M) . [n,('G' B)] = 1 ) by XBOOLEAN:def 3;
suppose (SAT M) . [n,('G' B)] = 0 ; :: thesis: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
hence (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1 by A1; :: thesis: verum
end;
suppose A2: (SAT M) . [n,('G' B)] = 1 ; :: thesis: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
now :: thesis: for i being Element of NAT holds (SAT M) . [((n + 1) + i),B] = 1
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;
then (SAT M) . [(n + 1),('G' B)] = 1 by Th10;
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;
end;