defpred S_{1}[ set , set ] means $1 = 0 ;

consider X being non empty strict ARS such that

A1: the carrier of X = {0,1} and

A2: for x, y being Element of X holds

( x ==> y iff S_{1}[x,y] )
from ABSRED_0:sch 7();

reconsider z = 0 , o = 1 as Element of X by A1, TARSKI:def 2;

A3: z <> o ;

take X ; :: thesis: ( X is WN & not X is SN )

thus X is WN :: thesis: not X is SN

A4: z in {z} by TARSKI:def 1;

consider X being non empty strict ARS such that

A1: the carrier of X = {0,1} and

A2: for x, y being Element of X holds

( x ==> y iff S

reconsider z = 0 , o = 1 as Element of X by A1, TARSKI:def 2;

A3: z <> o ;

take X ; :: thesis: ( X is WN & not X is SN )

thus X is WN :: thesis: not X is SN

proof

set A = {z};
let x be Element of X; :: according to ABSRED_0:def 14 :: thesis: x is normalizable

( x = 0 or x = 1 ) by A1, TARSKI:def 2;

then ( x is normform or x is normalizable ) by A2, A3, LmA;

hence x is normalizable ; :: thesis: verum

end;( x = 0 or x = 1 ) by A1, TARSKI:def 2;

then ( x is normform or x is normalizable ) by A2, A3, LmA;

hence x is normalizable ; :: thesis: verum

A4: z in {z} by TARSKI:def 1;

now :: thesis: for x being Element of X st x in {z} holds

ex y being Element of X st

( y in {z} & x ==> y )

hence
not X is SN
by A4, ThSN; :: thesis: verumex y being Element of X st

( y in {z} & x ==> y )

let x be Element of X; :: thesis: ( x in {z} implies ex y being Element of X st

( y in {z} & x ==> y ) )

assume x in {z} ; :: thesis: ex y being Element of X st

( y in {z} & x ==> y )

then A5: x = z by TARSKI:def 1;

take y = z; :: thesis: ( y in {z} & x ==> y )

thus ( y in {z} & x ==> y ) by A2, A5, TARSKI:def 1; :: thesis: verum

end;( y in {z} & x ==> y ) )

assume x in {z} ; :: thesis: ex y being Element of X st

( y in {z} & x ==> y )

then A5: x = z by TARSKI:def 1;

take y = z; :: thesis: ( y in {z} & x ==> y )

thus ( y in {z} & x ==> y ) by A2, A5, TARSKI:def 1; :: thesis: verum