per
cases
(
u
=
0.
Z_2
or
u
=
1.
Z_2
)
by
BSPACE:5
,
BSPACE:6
,
XBOOLEAN:def 3
;
suppose
A2
:
u
=
0.
Z_2
;
:: thesis:
u
*
v
=
u
'&'
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
'&'
v
then
u
*
v
=
(
0.
Z_2
)
*
(
0.
Z_2
)
.=
0
by
BSPACE:5
;
hence
u
*
v
=
u
'&'
v
by
A2
;
:: thesis:
verum
end;
suppose
v
=
1.
Z_2
;
:: thesis:
u
*
v
=
u
'&'
v
u
*
v
=
(
0.
Z_2
)
*
(
1.
Z_2
)
by
A2
.=
0
by
BSPACE:5
;
hence
u
*
v
=
u
'&'
v
by
A2
;
:: thesis:
verum
end;
end;
end;
suppose
A3
:
u
=
1.
Z_2
;
:: thesis:
u
*
v
=
u
'&'
v
per
cases
(
v
=
0.
Z_2
or
v
=
1.
Z_2
)
by
BSPACE:5
,
BSPACE:6
,
XBOOLEAN:def 3
;
suppose
A4
:
v
=
0.
Z_2
;
:: thesis:
u
*
v
=
u
'&'
v
then
u
*
v
=
(
1.
Z_2
)
*
(
0.
Z_2
)
.=
0
by
BSPACE:5
;
hence
u
*
v
=
u
'&'
v
by
A4
;
:: thesis:
verum
end;
suppose
v
=
1.
Z_2
;
:: thesis:
u
*
v
=
u
'&'
v
hence
u
*
v
=
u
'&'
v
by
A3
;
:: thesis:
verum
end;
end;
end;
end;