---

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


1. [opr] : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
⊢ ∀t:term(opr). (↑wf-term(arity;sort;t) ⇐⇒ hereditarily(opr;s.correct-sort-arity(sort;arity;s);t))
BY
{ (BLemma `term-induction`
   THEN Auto
   THEN ((RWO "assert-wf-mkterm" 0 THENA Auto)
   ORELSE (RWO "hereditarily-varterm hereditarily-mkterm" 0
           THEN Auto
           THEN ((RWO "assert-wf-mkterm" 7 THENA Auto)
           ORELSE (RepUR ``correct-sort-arity`` 0 THEN RepUR ``isvarterm varterm`` 0 THEN Auto)
           ))
   )
   THEN Try ((BackThruSomeHyp THEN Auto THEN RepeatFor 2 (D -1) THEN RWO "-1" 0 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. (||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])))))
⊢ correct-sort-arity(sort;arity;mkterm(f;bts))

2
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])))))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  sort  :  term(opr)  {}\mrightarrow{}  \mBbbN{}
3.  arity  :  opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)
\mvdash{}  \mforall{}t:term(opr).  (\muparrow{}wf-term(arity;sort;t)  \mLeftarrow{}{}\mRightarrow{}  hereditarily(opr;s.correct-sort-arity(sort;arity;s);t))


By

---

Latex:
(BLemma  `term-induction`
  THEN  Auto
  THEN  ((RWO  "assert-wf-mkterm"  0  THENA  Auto)
  ORELSE  (RWO  "hereditarily-varterm  hereditarily-mkterm"  0
                  THEN  Auto
                  THEN  ((RWO  "assert-wf-mkterm"  7  THENA  Auto)
                  ORELSE  (RepUR  ``correct-sort-arity``  0  THEN  RepUR  ``isvarterm  varterm``  0  THEN  Auto)
                  ))
  )
  THEN  Try  ((BackThruSomeHyp  THEN  Auto  THEN  RepeatFor  2  (D  -1)  THEN  RWO  "-1"  0  THEN  Auto)))

---

Home Index