let i be Element of NAT ; :: thesis: ( {(prop i)} |- 'G' (prop i) & not {(prop i)} |-0 'G' (prop i) )
thus {(prop i)} |- 'G' (prop i) :: thesis: not {(prop i)} |-0 'G' (prop i)
proof
prop i in {(prop i)} by TARSKI:def 1;
then {(prop i)} |- prop i by LTLAXIO1:42;
hence {(prop i)} |- 'G' (prop i) by LTLAXIO1:54; :: thesis: verum
end;
thus not {(prop i)} |-0 'G' (prop i) :: thesis: verum
proof
assume {(prop i)} |-0 'G' (prop i) ; :: thesis: contradiction
then A2: {(prop i)} |=0 'G' (prop i) by th266;
not {(prop i)} |=0 'X' (prop i) by th268, th14;
then consider M being LTLModel such that
A1: ( M |=0 {(prop i)} & not M |=0 'X' (prop i) ) ;
M |=0 'G' (prop i) by A2, A1;
then (SAT M) . [(0 + 1),(prop i)] = 1 by LTLAXIO1:10;
hence contradiction by LTLAXIO1:9, A1; :: thesis: verum
end;