reconsider R = {[0,1]} as non empty Relation ;
take R ; :: thesis: R is complete
A1: field R = {0,1} by RELAT_1:17;
thus R is confluent :: according to REWRITE1:def 25 :: thesis: R is strongly-normalizing

proof

let a, b be object ; :: according to REWRITE1:def 22 :: thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
given c being object such that A2: R reduces c,a and
A3: R reduces c,b ; :: according to REWRITE1:def 8 :: thesis: a,b are_convergent_wrt R

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: a,b are_convergent_wrt R

hence a,b are_convergent_wrt R by Th38; :: thesis: verum

end;

suppose a <> b ; :: thesis: a,b are_convergent_wrt R

then ( a <> c or b <> c ) ;
then A4: c in field R by A2, A3, Th18;
then a in {0,1} by A1, A2, Th18;
then A5: ( a = 0 or a = 1 ) by TARSKI:def 2;
b in {0,1} by A1, A3, A4, Th18;
then A6: ( b = 0 or b = 1 ) by TARSKI:def 2;
[0,1] in R by TARSKI:def 1;
then A7: R reduces 0 ,1 by Th15;
R reduces 1,1 by Th12;
hence a,b are_convergent_wrt R by A5, A6, A7; :: thesis: verum

end;

end;

end;

A8: R is co-well_founded

proof

let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( Y c= field R & Y <> {} implies ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) ) )
assume that
A9: Y c= field R and
A10: Y <> {} ; :: thesis: ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) )
reconsider Y9 = Y as non empty set by A10;
set y = the Element of Y9;

per cases ( 1 in Y or ( not 1 in Y & the Element of Y9 in Y ) ) ;

suppose A11: 1 in Y ; :: thesis: ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) )

take 1 ; :: thesis: ( 1 in Y & ( for b being object st b in Y & 1 <> b holds
not [1,b] in R ) )
thus 1 in Y by A11; :: thesis: for b being object st b in Y & 1 <> b holds
not [1,b] in R
let b be object ; :: thesis: ( b in Y & 1 <> b implies not [1,b] in R )
assume that
b in Y and
1 <> b ; :: thesis: not [1,b] in R
[0,1] <> [1,b] by XTUPLE_0:1;
hence not [1,b] in R by TARSKI:def 1; :: thesis: verum

end;

suppose A12: ( not 1 in Y & the Element of Y9 in Y ) ; :: thesis: ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) )

take 0 ; :: thesis: ( 0 in Y & ( for b being object st b in Y & 0 <> b holds
not [0,b] in R ) )
thus 0 in Y by A1, A9, A12, TARSKI:def 2; :: thesis: for b being object st b in Y & 0 <> b holds
not [0,b] in R
let b be object ; :: thesis: ( b in Y & 0 <> b implies not [0,b] in R )
assume b in Y ; :: thesis: ( not 0 <> b or not [0,b] in R )
hence ( not 0 <> b or not [0,b] in R ) by A1, A9, A12, TARSKI:def 2; :: thesis: verum

end;

end;

end;

R is irreflexive

proof

let x be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( not x in field R or not [x,x] in R )
assume that
x in field R and
A13: [x,x] in R ; :: thesis: contradiction
A14: [x,x] = [0,1] by A13, TARSKI:def 1;
then x = 0 by XTUPLE_0:1;
hence contradiction by A14, XTUPLE_0:1; :: thesis: verum

end;

hence R is strongly-normalizing by A8; :: thesis: verum