それでは，次に，後ろ向きの帰納法を find_theorems name: induct "?P (Suc ?n) ==> ?P ?n" のように探してみると searched for: name: "induct" "?P (Suc ?n) ⟹ ?P ?n"found 4 theorem(s):Nat.inc_induct: ?i ≤ ?j ⟹ ?P ?j ⟹ (⋀i. i Nat.strict_inc_induct:…

ということで，次は have "... ですが，今回はsimpを試すまでももなく Suc.hyps: ∀k. 0 ≤ a k ⟹ GM a ?m (2 ^ N) ≤ AM a ?m (2 ^ N) Suc.prems: ∀k. 0 ≤ a k を用いる訳で，そのためにthoremレベルのinst属性であるOF，および，termレベルのinst属性であるof…

ということでamgm2は準備出来たのですが，今度はGMがその仮定を満たすこと，つまり lemma GMge0: "ALL k. 0 0 0 GM a m n" が入用になります．例によって proof simp と試すと goal (1 subgoal): 1. ∀k. 0 ≤ a k ⟹ 0 までは出来ているので find_theorems "0 …

この結果の右辺は引き続き用いるので also とすれば calculation: GM a m (2 ^ Suc N) = root 2 (GM a m (2 ^ N) * GM a (m + 2 ^ N) (2 ^ N)) のように記憶され，右辺が...で参照できます． 従って，次は have "... GM a m (2 ^ N) + GM a (m + 2 ^ N) (2 ^…

よって今度は find_theorems "setprod ?f ?A * setprod ?f ?B" とすれば使えそうな定理 Big_Operators.setprod_Un_disjoint: finite ?A ⟹ finite ?B ⟹ ?A ∩ ?B = {} ⟹ setprod ?g (?A ∪ ?B) = setprod ?g ?A * setprod ?g ?B が見付かりますので，これを用い…