let H be CTL-formula; :: thesis: for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= 'not' H iff s,kai |/= H )
let S be non empty set ; :: thesis: for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= 'not' H iff s,kai |/= H )
let R be total Relation of S,S; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= 'not' H iff s,kai |/= H )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= 'not' H iff s,kai |/= H )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= 'not' H iff s,kai |/= H )
let kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)); :: thesis: ( s,kai |= 'not' H iff s,kai |/= H )
( s,kai |= 'not' H iff s |= 'not' (Evaluate (H,kai)) ) by Th5;
then ( s,kai |= 'not' H iff s |/= Evaluate (H,kai) ) by Th12;
hence ( s,kai |= 'not' H iff s,kai |/= H ) ; :: thesis: verum