Lean4
/-- We have partitioned the TM2 statements into "stack actions", which require going to the end
of the stack, and all other actions, which do not. This is a modified recursor which lumps the
stack actions into one. -/
@[elab_as_elim]
def stmtStRec.{l} {motive : TM2.Stmt Γ Λ σ → Sort l}
(run : ∀ (k) (s : StAct K Γ σ k) (q) (_ : motive q), motive (stRun s q))
(load : ∀ (a q) (_ : motive q), motive (TM2.Stmt.load a q))
(branch : ∀ (p q₁ q₂) (_ : motive q₁) (_ : motive q₂), motive (TM2.Stmt.branch p q₁ q₂))
(goto : ∀ l, motive (TM2.Stmt.goto l)) (halt : motive TM2.Stmt.halt) : ∀ n, motive n
| TM2.Stmt.push _ f q => run _ (push f) _ (stmtStRec run load branch goto halt q)
| TM2.Stmt.peek _ f q => run _ (peek f) _ (stmtStRec run load branch goto halt q)
| TM2.Stmt.pop _ f q => run _ (pop f) _ (stmtStRec run load branch goto halt q)
| TM2.Stmt.load _ q => load _ _ (stmtStRec run load branch goto halt q)
| TM2.Stmt.branch _ q₁ q₂ =>
branch _ _ _ (stmtStRec run load branch goto halt q₁) (stmtStRec run load branch goto halt q₂)
| TM2.Stmt.goto _ => goto _
| TM2.Stmt.halt => halt
