per
cases
(
u
=
0.
Z_2
or
u
=
1.
Z_2
)
by
BSPACE:5
,
BSPACE:6
,
XBOOLEAN:def 3
;
suppose
u
=
0.
Z_2
;
:: thesis:
u
+
v
=
u
'xor'
v
hence
u
+
v
=
u
'xor'
v
by
RLVECT_1:4
,
BSPACE:5
;
:: thesis:
verum
end;
suppose
A1
:
u
=
1.
Z_2
;
:: thesis:
u
+
v
=
u
'xor'
v
per
cases
(
v
=
0.
Z_2
or
v
=
1.
Z_2
)
by
BSPACE:5
,
BSPACE:6
,
XBOOLEAN:def 3
;
suppose
v
=
0.
Z_2
;
:: thesis:
u
+
v
=
u
'xor'
v
hence
u
+
v
=
u
'xor'
v
by
RLVECT_1:4
,
BSPACE:5
;
:: thesis:
verum
end;
suppose
v
=
1.
Z_2
;
:: thesis:
u
+
v
=
u
'xor'
v
hence
u
+
v
=
u
'xor'
v
by
A1
,
BSPACE:5
,
BSPACE:7
,
XBOOLEAN:147
;
:: thesis:
verum
end;
end;
end;
end;