---

Step * 2 1 1 1 2 of Lemma wfbts_wf


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|| ∈ ℤ
11. ∀i:ℕ||bts||
      ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ)
      ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ)
      ∧ (↑wf-term(arity;sort;snd(bts[i]))))
12. wfbts(t) = bts ∈ (bound-term(opr) List)
13. L : bound-term(opr) List
14. wfbts(t) = L ∈ (bound-term(opr) List)
15. L = bts ∈ (bound-term(opr) List)
16. term-opr(t) = f ∈ opr
⊢ ∀i:ℕ||L||
    ((||fst(L[i])|| = (fst(arity term-opr(t)[i])) ∈ ℤ) ∧ ((sort (snd(L[i]))) = (snd(arity term-opr(t)[i])) ∈ ℤ))
BY
{ (ParallelOp -6 THEN D -1) }

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|| ∈ ℤ
11. ∀i:ℕ||bts||
      ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ)
      ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ)
      ∧ (↑wf-term(arity;sort;snd(bts[i]))))
12. wfbts(t) = bts ∈ (bound-term(opr) List)
13. L : bound-term(opr) List
14. wfbts(t) = L ∈ (bound-term(opr) List)
15. L = bts ∈ (bound-term(opr) List)
16. term-opr(t) = f ∈ opr
17. i : ℕ||L||
18. ||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ
19. ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ) ∧ (↑wf-term(arity;sort;snd(bts[i])))
⊢ (||fst(L[i])|| = (fst(arity term-opr(t)[i])) ∈ ℤ) ∧ ((sort (snd(L[i]))) = (snd(arity term-opr(t)[i])) ∈ ℤ)

---

Latex:

---

Latex:

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||
11.  \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]))))
12.  wfbts(t)  =  bts
13.  L  :  bound-term(opr)  List
14.  wfbts(t)  =  L
15.  L  =  bts
16.  term-opr(t)  =  f
\mvdash{}  \mforall{}i:\mBbbN{}||L||
        ((||fst(L[i])||  =  (fst(arity  term-opr(t)[i])))
        \mwedge{}  ((sort  (snd(L[i])))  =  (snd(arity  term-opr(t)[i]))))


By

---

Latex:
(ParallelOp  -6  THEN  D  -1)

---

Home Index