let n be Element of NAT ; :: thesis: ( {(prop n)} |= 'X' (prop n) & not {(prop n)} |=0 'X' (prop n) )
thus {(prop n)} |= 'X' (prop n) :: thesis: not {(prop n)} |=0 'X' (prop n)
proof
let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( not M |= {(prop n)} or M |= 'X' (prop n) )
assume M |= {(prop n)} ; :: thesis: M |= 'X' (prop n)
then A2: M |= prop n by LTLAXIO1:23;
let i be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [i,('X' (prop n))] = 1
(SAT M) . [(i + 1),(prop n)] = 1 by A2;
hence (SAT M) . [i,('X' (prop n))] = 1 by LTLAXIO1:9; :: thesis: verum
end;
thus not {(prop n)} |=0 'X' (prop n) :: thesis: verum
proof
defpred S1[ Element of NAT , Element of bool props] means ( ( $1 = 0 implies $2 = {(prop n)} ) & ( not $1 = 0 implies $2 = {} LTLB_WFF ) );
A3: for x being Element of NAT ex y being Element of bool props st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of bool props st S1[x,y]
per cases ( x = 0 or not x = 0 ) ;
suppose S1: x = 0 ; :: thesis: ex y being Element of bool props st S1[x,y]
prop n in props by LTLAXIO1:def 10;
then reconsider p0 = {(prop n)} as Element of bool props by ZFMISC_1:31;
S1[x,p0] by S1;
hence ex y being Element of bool props st S1[x,y] ; :: thesis: verum
end;
suppose S2: not x = 0 ; :: thesis: ex y being Element of bool props st S1[x,y]
reconsider e = {} LTLB_WFF as Element of bool props by XBOOLE_1:2;
S1[x,e] by S2;
hence ex y being Element of bool props st S1[x,y] ; :: thesis: verum
end;
end;
end;
consider M being Function of NAT,(bool props) such that
A4: for x being Element of NAT holds S1[x,M . x] from FUNCT_2:sch 3(A3);
 reconsider M = M as LTLModel ;
A5: M |=0 {(prop n)}
proof
let A be Element of LTLB_WFF ; :: according to LTLAXIO5:def 2 :: thesis: ( A in {(prop n)} implies M |=0 A )
assume A in {(prop n)} ; :: thesis: M |=0 A
then A6: A = prop n by TARSKI:def 1;
M . 0 = {(prop n)} by A4;
then prop n in M . 0 by TARSKI:def 1;
hence M |=0 A by LTLAXIO1:def 11, A6; :: thesis: verum
end;
not M |=0 'X' (prop n)
proof
assume M |=0 'X' (prop n) ; :: thesis: contradiction
then (SAT M) . [(0 + 1),(prop n)] = 1 by LTLAXIO1:9;
then prop n in M . 1 by LTLAXIO1:def 11;
hence contradiction by A4; :: thesis: verum
end;
hence not {(prop n)} |=0 'X' (prop n) by A5; :: thesis: verum
end;