let A, B be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |=0 'G' (A => B) & F |=0 'G' (A => ('X' A)) holds
F |=0 'G' (A => ('G' B))
let F be Subset of LTLB_WFF; :: thesis: ( F |=0 'G' (A => B) & F |=0 'G' (A => ('X' A)) implies F |=0 'G' (A => ('G' B)) )
assume that
A1: F |=0 'G' (A => B) and
A2: F |=0 'G' (A => ('X' A)) ; :: thesis: F |=0 'G' (A => ('G' B))
let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 'G' (A => ('G' B)) )
assume A3: M |=0 F ; :: thesis: M |=0 'G' (A => ('G' B))
now :: thesis: for n being Element of NAT holds (SAT M) . [(0 + n),(A => ('G' B))] = 1
let n be Element of NAT ; :: thesis: (SAT M) . [(0 + b1),(A => ('G' B))] = 1
defpred S1[ 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 A4: (SAT M) . [n,A] = 1 ; :: thesis: (SAT M) . [(0 + b1),(A => ('G' B))] = 1
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
M |=0 'G' (A => ('X' A)) by A2, A3;
then (SAT M) . [(0 + (n + kk)),(A => ('X' A))] = 1 by LTLAXIO1:10;
then ((SAT M) . [(n + kk),A]) => ((SAT M) . [(n + kk),('X' A)]) = 1 by LTLAXIO1:def 11;
then (SAT M) . [((n + kk) + 1),A] = 1 by A6, LTLAXIO1:9;
hence S1[k + 1] ; :: thesis: verum
end;
A7: S1[ 0 ] by A4;
A8: for i being Nat holds S1[i] from NAT_1:sch 2(A7, A5);
now :: thesis: for i being Element of NAT holds (SAT M) . [(n + i),B] = 1
let i be Element of NAT ; :: thesis: (SAT M) . [(n + i),B] = 1
M |=0 'G' (A => B) by A1, A3;
then (SAT M) . [(0 + (n + i)),(A => B)] = 1 by LTLAXIO1:10;
then A9: ((SAT M) . [(n + i),A]) => ((SAT M) . [(n + i),B]) = 1 by LTLAXIO1:def 11;
(SAT M) . [(n + i),A] = 1 by A8;
hence (SAT M) . [(n + i),B] = 1 by A9; :: thesis: verum
end;
then (SAT M) . [n,('G' B)] = 1 by LTLAXIO1:10;
then ((SAT M) . [n,A]) => ((SAT M) . [n,('G' B)]) = 1 ;
hence (SAT M) . [(0 + n),(A => ('G' B))] = 1 by LTLAXIO1:def 11; :: thesis: verum
end;
suppose (SAT M) . [n,A] = 0 ; :: thesis: (SAT M) . [(0 + b1),(A => ('G' B))] = 1
then ((SAT M) . [n,A]) => ((SAT M) . [n,('G' B)]) = 1 ;
hence (SAT M) . [(0 + n),(A => ('G' B))] = 1 by LTLAXIO1:def 11; :: thesis: verum
end;
end;
end;
hence M |=0 'G' (A => ('G' B)) by LTLAXIO1:10; :: thesis: verum