学籍番号::
名前::
以下の文章は命題の証明と、それをMizarで表したものである。
内の字句を埋め、Mizarのテキストを完成させて下さい。
解答は[1]〜[4]の順にアルファベットを続けて入力して下さい
証明
証明終了
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 :: AMI_5'2:
X c= Y implies X c= Z \/ Y
proof
assume [1]; then
A1: [2] c= [3] by BOOLE'33;
[4] \/ X by BOOLE'31;
hence X c= Z \/ Y by A1,BOOLE'29;
end;
[選択肢]
[a] Z \/ Y
[b] Z \/ X
[c] X c= Z
[d] X c= Y
[1]
[2]
[3]
[4]