2011-11-19から1日間の記事一覧
通常の帰納法の原理 # num_INDUCTION;; val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n) を用いて,Wellfounded induction(整礎帰納法)の原理 # num_WF;; val it : thm = |- !P. (!n. (!m. m P m) ==> P n) ==> (!n. P n) を証明して…
通常の帰納法の原理 # num_INDUCTION;; val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n) を用いて,Wellfounded induction(整礎帰納法)の原理 # num_WF;; val it : thm = |- !P. (!n. (!m. m P m) ==> P n) ==> (!n. P n) を証明して…