---

Step * of Lemma int-term-ind-fun_wf

∀[A:Type]. ∀[v:int_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply:left:int_term()
                                                                                ⟶ right:int_term()
                                                                                ⟶ A
                                                                                ⟶ A
                                                                                ⟶ A].
∀[Minus:num:int_term() ⟶ A ⟶ A].
  (int-term-ind-fun(c.Constant[c];
                    v.Var[v];
                    l,r,rl,rr.Add[l;r;rl;rr];
                    l,r,rl,rr.Subtract[l;r;rl;rr];
                    l,r,rl,rr.Multiply[l;r;rl;rr];
                    x,rx.Minus[x;rx]) ∈ int_term() ⟶ A)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[v:int\_term()].  \mforall{}[Constant,Var:var:\mBbbZ{}  {}\mrightarrow{}  A].  \mforall{}[Add,Subtract,Multiply:left:int\_term()
                                                                                                                                                                {}\mrightarrow{}  right:int\_term()
                                                                                                                                                                {}\mrightarrow{}  A
                                                                                                                                                                {}\mrightarrow{}  A
                                                                                                                                                                {}\mrightarrow{}  A].
\mforall{}[Minus:num:int\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (int-term-ind-fun(c.Constant[c];
                                        v.Var[v];
                                        l,r,rl,rr.Add[l;r;rl;rr];
                                        l,r,rl,rr.Subtract[l;r;rl;rr];
                                        l,r,rl,rr.Multiply[l;r;rl;rr];
                                        x,rx.Minus[x;rx])  \mmember{}  int\_term()  {}\mrightarrow{}  A)


By

---

Latex:
ProveWfLemma

---

Home Index