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

proof

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

per cases ;

suppose a = b ; :: thesis:

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

end;

suppose a <> b ; :: thesis:

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:

end;

end;

end;

A8: R is co-well_founded

proof

let Y be set ; :: according to REWRITE1:def 16 :: thesis:
assume that
A9: Y c= field R and
A10: Y <> {} ; :: thesis:
reconsider Y9 = Y as non empty set by A10;
set y = the Element of Y9;

per cases ;

suppose A11: 1 in Y ; :: thesis:

take 1 ; :: thesis:
thus 1 in Y by A11; :: thesis:
let b be object ; :: thesis:
assume that
b in Y and
1 <> b ; :: thesis:
[0,1] <> [1,b] by XTUPLE_0:1;
hence not [1,b] in R by TARSKI:def 1; :: thesis:

end;

suppose A12: ( not 1 in Y & the Element of Y9 in Y ) ; :: thesis:

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

end;

end;

end;

R is irreflexive

proof

let x be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis:
assume that
x in field R and
A13: [x,x] in R ; :: thesis:
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:

end;

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