---

Step * of Lemma wfbts_wf

No Annotations
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[t:wfterm(opr;sort;arity)].
  wfbts(t) ∈ wf-bound-terms(opr;sort;arity;term-opr(t)) supposing ¬↑isvarterm(t)
BY
{ (Auto
   THEN DupHyp (-1)
   THEN (RWO "assert-not-isvarterm" (-1) THENA Auto)
   THEN ExRepD
   THEN DVar `t'
   THEN (Assert ↑wf-term(arity;sort;mkterm(f;bts)) BY
               Auto)
   THEN (RWO "assert-wf-mkterm" (-1) THENA Auto)
   THEN (MemTypeCD THENW Auto)) }

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

2
.....set predicate..... 
1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
4. t : term(opr)
5. ↑wf-term(arity;sort;t)
6. ¬↑isvarterm(t)
7. f : opr
8. bts : bound-term(opr) List
9. t = mkterm(f;bts) ∈ term(opr)
10. (||bts|| = ||arity f|| ∈ ℤ)
∧ (∀i:ℕ||bts||
     ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ)
     ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ)
     ∧ (↑wf-term(arity;sort;snd(bts[i])))))
⊢ (||wfbts(t)|| = ||arity term-opr(t)|| ∈ ℤ)
∧ (∀i:ℕ||wfbts(t)||
     ((||fst(wfbts(t)[i])|| = (fst(arity term-opr(t)[i])) ∈ ℤ)
     ∧ ((sort (snd(wfbts(t)[i]))) = (snd(arity term-opr(t)[i])) ∈ ℤ)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[sort:term(opr)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)].  \mforall{}[t:wfterm(opr;sort;arity)].
    wfbts(t)  \mmember{}  wf-bound-terms(opr;sort;arity;term-opr(t))  supposing  \mneg{}\muparrow{}isvarterm(t)


By

---

Latex:
(Auto
  THEN  DupHyp  (-1)
  THEN  (RWO  "assert-not-isvarterm"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  DVar  `t'
  THEN  (Assert  \muparrow{}wf-term(arity;sort;mkterm(f;bts))  BY
                          Auto)
  THEN  (RWO  "assert-wf-mkterm"  (-1)  THENA  Auto)
  THEN  (MemTypeCD  THENW  Auto))

---

Home Index