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)

thus {(prop n)} |= 'X' (prop n) :: thesis: not {(prop n)} |=0 'X' (prop n)

proof

thus
not {(prop n)} |=0 'X' (prop n)
:: thesis: verum
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;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

proof

defpred S_{1}[ 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 S_{1}[x,y]

A4: for x being Element of NAT holds S_{1}[x,M . x]
from FUNCT_2:sch 3(A3);

reconsider M = M as LTLModel ;

A5: M |=0 {(prop n)}

end;A3: for x being Element of NAT ex y being Element of bool props st S

proof

consider M being Function of NAT,(bool props) such that
let x be Element of NAT ; :: thesis: ex y being Element of bool props st S_{1}[x,y]

end;per cases
( x = 0 or not x = 0 )
;

end;

suppose S1:
x = 0
; :: thesis: ex y being Element of bool props st S_{1}[x,y]

prop n in props
by LTLAXIO1:def 10;

then reconsider p0 = {(prop n)} as Element of bool props by ZFMISC_1:31;

S_{1}[x,p0]
by S1;

hence ex y being Element of bool props st S_{1}[x,y]
; :: thesis: verum

end;then reconsider p0 = {(prop n)} as Element of bool props by ZFMISC_1:31;

S

hence ex y being Element of bool props st S

suppose S2:
not x = 0
; :: thesis: ex y being Element of bool props st S_{1}[x,y]

reconsider e = {} LTLB_WFF as Element of bool props by XBOOLE_1:2;

S_{1}[x,e]
by S2;

hence ex y being Element of bool props st S_{1}[x,y]
; :: thesis: verum

end;S

hence ex y being Element of bool props st S

A4: for x being Element of NAT holds S

reconsider M = M as LTLModel ;

A5: M |=0 {(prop n)}

proof

not M |=0 'X' (prop n)
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;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

proof

hence
not {(prop n)} |=0 'X' (prop n)
by A5; :: thesis: verum
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;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