---

Step * 1 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. 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)>]
BY
{ (BackThruSomeHyp 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
13. bt : bound-term(opr)
14. (bt ∈ bts)
⊢ P[bt]

---

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.  n  :  \mBbbN{}
6.  \mforall{}n:\mBbbN{}n.  \mforall{}bt:bound-term(opr).    ((bound-term-size(bt)  \mleq{}  n)  {}\mRightarrow{}  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)
12.  bound-term-size(<b1,  b2>)  \mleq{}  n
\mvdash{}  P[<b1,  mkterm(f;bts)>]


By

---

Latex:
(BackThruSomeHyp  THEN  Auto)

---

Home Index