---

Step * of Lemma mkwfterm_wf

No Annotations
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[f:opr]. ∀[bts:wf-bound-terms(opr;sort;arity;f)].
  (mkwfterm(f;bts) ∈ wfterm(opr;sort;arity))
BY
{ (Unfold `mkwfterm` 0 THEN Auto THEN D -1 THEN MemTypeCD THEN Auto THEN BLemma `assert-wf-mkterm` THEN Auto) }

1
1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
4. f : opr
5. bts : (varname() List × wfterm(opr;sort;arity)) List
6. ||bts|| = ||arity f|| ∈ ℤ
7. ∀i:ℕ||bts||. ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ) ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ))
8. ||bts|| = ||arity f|| ∈ ℤ
9. i : ℕ||bts||
10. ||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ
11. (sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ
⊢ ↑wf-term(arity;sort;snd(bts[i]))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[sort:term(opr)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)].  \mforall{}[f:opr].
\mforall{}[bts:wf-bound-terms(opr;sort;arity;f)].
    (mkwfterm(f;bts)  \mmember{}  wfterm(opr;sort;arity))


By

---

Latex:
(Unfold  `mkwfterm`  0
  THEN  Auto
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  BLemma  `assert-wf-mkterm`
  THEN  Auto)

---

Home Index