environ
vocabularies HIDDEN, RELAT_1, XBOOLE_0, FUNCT_1, REWRITE1, TDGROUP, ABSRED_0, ZFMISC_1, FINSEQ_1, ARYTM_1, SUBSET_1, NUMBERS, STRUCT_0, NAT_1, ARYTM_3, CARD_1, XXREAL_0, ZFREFLE1, TARSKI, UNIALG_1, GROUP_1, MSUALG_6, FUNCT_2, INCPROJ, EQREL_1, MSUALG_1, PARTFUN1, UNIALG_2, FUNCT_4, PBOOLE, FUNCT_7, FINSEQ_2, FUNCOP_1, ORDINAL1, MESFUNC1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, RELSET_1, FUNCT_1, SUBSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, EQREL_1, ORDINAL1, BINOP_1, FINSEQ_1, FINSEQ_2, NAT_1, FINSEQ_4, FUNCT_7, MARGREL1, STRUCT_0, PBOOLE, UNIALG_1, PUA2MSS1, REWRITE1;
definitions RELAT_1, MARGREL1, STRUCT_0, UNIALG_1, REWRITE1;
theorems ZFMISC_1, NAT_1, FINSEQ_3, FINSEQ_5, REWRITE1, IDEA_1, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, TARSKI, SUBSET_1, ENUMSET1, SETWISEO, ORDINAL1, SEQ_4, MARGREL1, RELSET_1, FINSEQ_1, PARTFUN1, FINSEQ_2, GRFUNC_1, FUNCOP_1, FUNCT_7, PUA2MSS1, COMPUT_1;
schemes NAT_1, RECDEF_1, RELSET_1;
registrations SUBSET_1, XBOOLE_0, RELSET_1, ORDINAL1, NAT_1, REWRITE1, XXREAL_0, XCMPLX_0, STRUCT_0, AOFA_A00, FUNCT_2, FINSEQ_1, FINSEQ_6, PARTFUN1, FUNCOP_1, FINSEQ_2, CARD_1, MARGREL1, UNIALG_1, PUA2MSS1, RELAT_1, REALSET1;
constructors HIDDEN, RELAT_1, RELSET_1, FUNCT_2, STRUCT_0, REWRITE1, XCMPLX_0, XXREAL_0, NAT_1, FINSEQ_5, ENUMSET1, BINOP_1, FINSEQ_1, FINSEQ_4, FUNCT_7, CARD_1, XXREAL_1, UNIALG_1, PUA2MSS1, REALSET1, MARGREL1, EQREL_1, NUMBERS, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, PARTFUN1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities EQREL_1;
expansions ;
scheme
Star{
F1()
-> ARS ,
P1[
object ] } :
for
x,
y being
Element of
F1() st
x =*=> y &
P1[
x] holds
P1[
y]
provided
A1:
for
x,
y being
Element of
F1() st
x ==> y &
P1[
x] holds
P1[
y]
scheme
StarBack{
F1()
-> ARS ,
P1[
object ] } :
for
x,
y being
Element of
F1() st
x =*=> y &
P1[
y] holds
P1[
x]
provided
A1:
for
x,
y being
Element of
F1() st
x ==> y &
P1[
y] holds
P1[
x]
definition
existence
ex b1 being strict ARS st
( the carrier of b1 = {0,1} & the reduction of b1 = [:{0},{0,1}:] )
uniqueness
for b1, b2 being strict ARS st the carrier of b1 = {0,1} & the reduction of b1 = [:{0},{0,1}:] & the carrier of b2 = {0,1} & the reduction of b2 = [:{0},{0,1}:] holds
b1 = b2
;
existence
ex b1 being strict ARS st
( the carrier of b1 = {0,1,2} & the reduction of b1 = [:{0},{0,1,2}:] )
uniqueness
for b1, b2 being strict ARS st the carrier of b1 = {0,1,2} & the reduction of b1 = [:{0},{0,1,2}:] & the carrier of b2 = {0,1,2} & the reduction of b2 = [:{0},{0,1,2}:] holds
b1 = b2
;
end;
theorem ThSN:
for
X being
ARS holds
(
X is
SN iff for
A being
set for
z being
Element of
X holds
( not
z in A or ex
x being
Element of
X st
(
x in A & ( for
y being
Element of
X holds
( not
y in A or not
x ==> y ) ) ) ) )
theorem
ex
X being
ARS st
(
X is
WN & not
X is
SN )
Lm3:
for X being ARS
for x, y being Element of X st x =*=> y holds
x <=*=> y
Lm2:
for X being ARS
for x, y being Element of X st x <<>> y holds
x <=*=> y
Lm1:
for X being ARS st X is CR holds
X is CONF
by Lm2;
:: x =+=> y implies x =*=> y;
:: x =+=> y & y =*=> z implies x =+=> z;
:: x =*=> y & y =+=> z implies x =+=> z;