2011-11-10から1日間の記事一覧
|- p ==> q と |- p から |- q を得るMP(: thm -> thm -> thm = )を用いる際 # LT_IMP_LE;; val it : thm = |- !m n. m m # MP (SPECL[`1`;`2`] it) (ARITH_RULE`1 val it : thm = |- 1 のように,SEPC(: term -> thm -> thm = ),SEPCL(: term list -> thm …
|- p ==> q と |- p から |- q を得るMP(: thm -> thm -> thm = )を用いる際 # LT_IMP_LE;; val it : thm = |- !m n. m m # MP (SPECL[`1`;`2`] it) (ARITH_RULE`1 val it : thm = |- 1 のように,SEPC(: term -> thm -> thm = ),SEPCL(: term list -> thm …