学籍番号::
名前::
以下の文章は命題の証明と、それをMizarで表したものである。
内の字句を埋め、Mizarのテキストを完成させて下さい。
解答は[1]〜[4]の順にアルファベットを続けて入力して下さい
証明
よってこれと(1)から
証明終了
environ
vocabulary BOOLE, ZFMISC_1;
notation TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
clusters XBOOLE_0;
requirements BOOLE;
begin
reserve x,A,B,X,X',Y,Y',Z,V for set;
theorem BOOLE'64: :: BOOLE'64:
(X \/ Y) \/ Z = X \/ (Y \/ Z)
proof
thus (X \/ Y) \/ Z c= X \/ (Y \/ Z)
proof let x;
assume [1] \/ Z;
then x in X \/ Y or x in Z by XBOOLE_0:def 2;
then [2] or x in Y or x in Z by XBOOLE_0:def 2;
then x in X or x in [3] by XBOOLE_0:def 2;
hence thesis by XBOOLE_0:def 2;
end;
let x;
assume x in X \/ (Y \/ Z);
then x in X or x in Y \/ Z by XBOOLE_0:def 2;
then x in X or x in Y or x in Z by XBOOLE_0:def 2;
then x in [4] or x in Z by XBOOLE_0:def 2;
hence thesis by XBOOLE_0:def 2;
end;
[選択肢]
[a] x in (X \/ Y)
[b] x in X
[c] Y \/ Z
[d] X \/ Y
[1]
[2]
[3]
[4]