---

Step * 1 of Lemma bound-term-induction


1. [opr] : Type
2. [P] : bound-term(opr) ⟶ ℙ
3. ∀vs:varname() List. ∀v:varname().  ((¬(v = nullvar() ∈ varname())) ⇒ P[<vs, varterm(v)>])
4. ∀bts:bound-term(opr) List
     ((∀bt:bound-term(opr). ((bt ∈ bts) ⇒ P[bt])) ⇒ (∀f:opr. ∀vs:varname() List.  P[<vs, mkterm(f;bts)>]))
5. bt : bound-term(opr)
⊢ P[bt]
BY
{ ((Enough to prove ∀n:ℕ. ∀bt:bound-term(opr).  ((bound-term-size(bt) ≤ n) ⇒ P[bt])
     Because (InstHyp [⌜bound-term-size(bt)⌝;⌜bt⌝] (-1)⋅ THEN Auto))
   THEN Thin (-1)
   THEN CompleteInductionOnNat
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (InstLemma `term-cases` [⌜opr⌝;⌜b2⌝]⋅ THENA Auto)
   THEN D -1
   THEN (ExRepD THENW (RepUR ``bound-term-size`` 0 THEN Auto))
   THEN RWO "-2" 0
   THEN Auto) }

1
1. [opr] : Type
2. [P] : bound-term(opr) ⟶ ℙ
3. ∀vs:varname() List. ∀v:varname().  ((¬(v = nullvar() ∈ varname())) ⇒ P[<vs, varterm(v)>])
4. ∀bts:bound-term(opr) List
     ((∀bt:bound-term(opr). ((bt ∈ bts) ⇒ P[bt])) ⇒ (∀f:opr. ∀vs:varname() List.  P[<vs, mkterm(f;bts)>]))
5. n : ℕ
6. ∀n:ℕn. ∀bt:bound-term(opr).  ((bound-term-size(bt) ≤ n) ⇒ P[bt])
7. b1 : varname() List
8. b2 : term(opr)
9. f : opr
10. bts : {bt:bound-term(opr)| bound-term-size(bt) < term-size(b2)}  List
11. b2 = mkterm(f;bts) ∈ term(opr)
12. bound-term-size(<b1, b2>) ≤ n
⊢ P[<b1, mkterm(f;bts)>]

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  [P]  :  bound-term(opr)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}vs:varname()  List.  \mforall{}v:varname().    ((\mneg{}(v  =  nullvar()))  {}\mRightarrow{}  P[<vs,  varterm(v)>])
4.  \mforall{}bts:bound-term(opr)  List
          ((\mforall{}bt:bound-term(opr).  ((bt  \mmember{}  bts)  {}\mRightarrow{}  P[bt]))
          {}\mRightarrow{}  (\mforall{}f:opr.  \mforall{}vs:varname()  List.    P[<vs,  mkterm(f;bts)>]))
5.  bt  :  bound-term(opr)
\mvdash{}  P[bt]


By

---

Latex:
((Enough  to  prove  \mforall{}n:\mBbbN{}.  \mforall{}bt:bound-term(opr).    ((bound-term-size(bt)  \mleq{}  n)  {}\mRightarrow{}  P[bt])
      Because  (InstHyp  [\mkleeneopen{}bound-term-size(bt)\mkleeneclose{};\mkleeneopen{}bt\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto))
  THEN  Thin  (-1)
  THEN  CompleteInductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (InstLemma  `term-cases`  [\mkleeneopen{}opr\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (ExRepD  THENW  (RepUR  ``bound-term-size``  0  THEN  Auto))
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index