---

Step * 1 of Lemma mkwfterm_wf


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]))
BY
{ ((GenConclTerm ⌜bts[i]⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN D -2 THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  sort  :  term(opr)  {}\mrightarrow{}  \mBbbN{}
3.  arity  :  opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)
4.  f  :  opr
5.  bts  :  (varname()  List  \mtimes{}  wfterm(opr;sort;arity))  List
6.  ||bts||  =  ||arity  f||
7.  \mforall{}i:\mBbbN{}||bts||.  ((||fst(bts[i])||  =  (fst(arity  f[i])))  \mwedge{}  ((sort  (snd(bts[i])))  =  (snd(arity  f[i]))))
8.  ||bts||  =  ||arity  f||
9.  i  :  \mBbbN{}||bts||
10.  ||fst(bts[i])||  =  (fst(arity  f[i]))
11.  (sort  (snd(bts[i])))  =  (snd(arity  f[i]))
\mvdash{}  \muparrow{}wf-term(arity;sort;snd(bts[i]))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}bts[i]\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  D  -2  THEN  Unhide  THEN  Auto)

---

Home Index