---

Step * 1 2 of Lemma wf-term-hereditarily-correct-sort-arity


1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
4. bts : bound-term(opr) List
5. ∀bt:bound-term(opr)
     ((bt ∈ bts) ⇒ (↑wf-term(arity;sort;snd(bt)) ⇐⇒ hereditarily(opr;s.correct-sort-arity(sort;arity;s);snd(bt))))
6. f : opr
7. hereditarily(opr;s.correct-sort-arity(sort;arity;s);mkterm(f;bts))
⊢ (||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])))))
BY
{ (DupHyp (-1)
   THEN D -1
   THEN RepUR ``correct-sort-arity isvarterm term-opr term-bts mkterm let`` -2
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

1
1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
4. bts : bound-term(opr) List
5. ∀bt:bound-term(opr)
     ((bt ∈ bts) ⇒ (↑wf-term(arity;sort;snd(bt)) ⇐⇒ hereditarily(opr;s.correct-sort-arity(sort;arity;s);snd(bt))))
6. f : opr
7. hereditarily(opr;s.correct-sort-arity(sort;arity;s);mkterm(f;bts))
8. (¬False)
⇒ ((||bts|| = ||arity f|| ∈ ℤ)
   ∧ (∀i:ℕ||bts||. ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ) ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ))))
9. ∀s:term(opr). (s << mkterm(f;bts) ⇒ correct-sort-arity(sort;arity;s))
10. ||bts|| = ||arity f|| ∈ ℤ
11. i : ℕ||bts||
12. ||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ
13. (sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ
⊢ hereditarily(opr;s.correct-sort-arity(sort;arity;s);snd(bts[i]))

---

Latex:

---

Latex:

1.  opr  :  Type
2.  sort  :  term(opr)  {}\mrightarrow{}  \mBbbN{}
3.  arity  :  opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)
4.  bts  :  bound-term(opr)  List
5.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)
          {}\mRightarrow{}  (\muparrow{}wf-term(arity;sort;snd(bt))
                \mLeftarrow{}{}\mRightarrow{}  hereditarily(opr;s.correct-sort-arity(sort;arity;s);snd(bt))))
6.  f  :  opr
7.  hereditarily(opr;s.correct-sort-arity(sort;arity;s);mkterm(f;bts))
\mvdash{}  (||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])))))


By

---

Latex:
(DupHyp  (-1)
  THEN  D  -1
  THEN  RepUR  ``correct-sort-arity  isvarterm  term-opr  term-bts  mkterm  let``  -2
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index