---

Step * 2 of Lemma wfbts_wf

.....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])) ∈ ℤ)))
BY
{ (Assert wfbts(t) = bts ∈ (bound-term(opr) List) BY
         (Unfold `wfbts` 0 THEN (RWO "-2" 0 THENA Auto) THEN RepUR ``term-bts mkterm`` 0 THEN 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])))))
11. wfbts(t) = bts ∈ (bound-term(opr) List)
⊢ (||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:
.....set  predicate..... 
1.  opr  :  Type
2.  sort  :  term(opr)  {}\mrightarrow{}  \mBbbN{}
3.  arity  :  opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)
4.  t  :  term(opr)
5.  \muparrow{}wf-term(arity;sort;t)
6.  \mneg{}\muparrow{}isvarterm(t)
7.  f  :  opr
8.  bts  :  bound-term(opr)  List
9.  t  =  mkterm(f;bts)
10.  (||bts||  =  ||arity  f||)
\mwedge{}  (\mforall{}i:\mBbbN{}||bts||
          ((||fst(bts[i])||  =  (fst(arity  f[i])))
          \mwedge{}  ((sort  (snd(bts[i])))  =  (snd(arity  f[i])))
          \mwedge{}  (\muparrow{}wf-term(arity;sort;snd(bts[i])))))
\mvdash{}  (||wfbts(t)||  =  ||arity  term-opr(t)||)
\mwedge{}  (\mforall{}i:\mBbbN{}||wfbts(t)||
          ((||fst(wfbts(t)[i])||  =  (fst(arity  term-opr(t)[i])))
          \mwedge{}  ((sort  (snd(wfbts(t)[i])))  =  (snd(arity  term-opr(t)[i])))))


By

---

Latex:
(Assert  wfbts(t)  =  bts  BY
              (Unfold  `wfbts`  0  THEN  (RWO  "-2"  0  THENA  Auto)  THEN  RepUR  ``term-bts  mkterm``  0  THEN  Auto))

---

Home Index