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 f being Assign of (CTLModel R,BASSIGN) holds
( s |= 'not' f iff s |/= f )
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 f being Assign of (CTLModel R,BASSIGN) holds
( s |= 'not' f iff s |/= f )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (CTLModel R,BASSIGN) holds
( s |= 'not' f iff s |/= f )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (CTLModel R,BASSIGN) holds
( s |= 'not' f iff s |/= f )
let f be Assign of (CTLModel R,BASSIGN); :: thesis: ( s |= 'not' f iff s |/= f )
A1: 'not' f = Not_0 f,S by Def43;
A2: ( s |= 'not' f implies s |/= f )

proof

assume s |= 'not' f ; :: thesis: s |/= f
then (Fid (Not_0 f,S),S) . s = TRUE by A1, Def59;
then 'not' (Castboolean ((Fid f,S) . s)) = TRUE by Def42;
then (Fid f,S) . s = FALSE by Def4;
hence s |/= f by Def59; :: thesis: verum

end;

( s |/= f implies s |= 'not' f )

proof

assume s |/= f ; :: thesis: s |= 'not' f
then not (Fid f,S) . s = TRUE by Def59;
then not Castboolean ((Fid f,S) . s) = TRUE by Def4;
then Castboolean ((Fid f,S) . s) = FALSE by XBOOLEAN:def 3;
then 'not' (Castboolean ((Fid f,S) . s)) = TRUE ;
then (Fid ('not' f),S) . s = TRUE by A1, Def42;
hence s |= 'not' f by Def59; :: thesis: verum

end;

hence ( s |= 'not' f iff s |/= f ) by A2; :: thesis: verum