|
⍺ ack ⍵ ←→ f⍢(3∘+) ⍵
⇒ (⍺+1)ack ⍵ ←→ f⍣(1+⍵)⍢(3∘+) 1
Proof: by induction on ⍵ .
| (⍺+1) ack 0 | basis |
| ⍺ ack 1 | definition of ack |
| f⍢(3∘+) 1 | antecedent of lemma |
| f⍣(1+0)⍢(3∘+) 1 | f ←→ f⍣1 |
| |
| (⍺+1) ack ⍵ | induction |
| ⍺ ack (⍺+1) ack ⍵-1 | definition of ack |
| f⍢(3∘+) (⍺+1) ack ⍵-1 | antecedent of lemma |
| f⍢(3∘+) f⍣(1+⍵-1)⍢(3∘+) 1 | inductive hypothesis |
| ¯3∘+ f 3∘+ ¯3∘+ f⍣(1+⍵-1) 3∘+ 1 | ⍢ |
| ¯3∘+ f f⍣(1+⍵-1) 3∘+ 1 | + |
| ¯3∘+ f⍣(1+⍵) 3∘+ 1 | ⍣ |
| f⍣(1+⍵)⍢(3∘+) 1 | ⍢ |
| QED |
|