2013-05-29から1日間の記事一覧
計算機を用いた定理証明における楽しみの1つは(参照先が見え難くなりますが)simplifyでしょう. lemma amgm_2_simps: fixes a m n shows "ALL k. 0 <= a k ==> GM a m (2 ^ n) <= AM a m (2 ^ n)" proof (induct n arbitrary: m) case 0 then show ?case …
計算機を用いた定理証明における楽しみの1つは(参照先が見え難くなりますが)simplifyでしょう. lemma amgm_2_simps: fixes a m n shows "ALL k. 0 <= a k ==> GM a m (2 ^ n) <= AM a m (2 ^ n)" proof (induct n arbitrary: m) case 0 then show ?case …