2013-05-09から1日間の記事一覧
さらに1つ目のサブゴールの証明は from 1 have "a 0 = 0" by simp also have "... = 1 - 1" by simp also have "... = 2 ^ 0 - 1" by simp finally show "a 0 = 2 ^ 0 - 1" by this のように,calculationを生成するコマンドalsoと,その結果をthisとして参…
さらに1つ目のサブゴールの証明は from 1 have "a 0 = 0" by simp also have "... = 1 - 1" by simp also have "... = 2 ^ 0 - 1" by simp finally show "a 0 = 2 ^ 0 - 1" by this のように,calculationを生成するコマンドalsoと,その結果をthisとして参…