証明パターンもっと 2 含意導入

はてなブログ 論理 本編ネタ お絵描き

\require{color} \newcommand{\hyp}{\mbox{-}}% \newcommand{\To}{\Rightarrow}% \newcommand{\F}[1]{ \langle\![{#1}]\!\rangle }% \newcommand{\As}{\;::\;}%

左含意導入

{\bf NDed}(A\land B, C) \to {\bf NDed}(B, A \to C)\mbox{ in }{\bf Set}\\ \:\\ \mbox{For } F:A\land B \to C \\ % % \xymatrix{%ソース \\ \\ \\ {}\ar[d]_-{A\land B} \\ *[F]{F} \ar[d]_-C \\ {} } \xymatrix{ %矢印 \\ \\ \\ {} \\ {} \ar@{|~>}[r] % リライト矢印 &{} \\ {} } % % 変形リーズニング % \xymatrix{%ターゲット {} &{} &{} \ar[d]_-B \\ {\textcolor{green}{\land}} %2,2 &{} &*[.]{}\ar[d] \\ *{\# 1}\ar[dr]_-{A} %3,2 &{} &*[.]{} \ar[dl]^-{B} \\ {} &*{\blacktriangledown} \ar[d]_{A\land B} &{} \\ {} &*[F]{F} \ar[d]_-{C} &{} \\ *{\# 1} &*+[o][F]{\to} \ar[d]_-{A\to C} \ar[l]_-{A} &{} \\ {} &*[.]{} \ar[d]_-{A\to C} &{} \\ {} & & \save "2,1" ."7,3" *\frm{.} \restore }