---

Step * 1 2 1 of Lemma subterm-mkterm


1. [opr] : Type
2. f : opr
3. bts : bound-term(opr) List
4. n : ℕ
5. ∀n:ℕn. ∀s:term(opr).
     (((term-size(mkterm(f;bts)) - term-size(s)) ≤ n)
     ⇒ s << mkterm(f;bts)
     ⇒ (∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))))
6. s : term(opr)
7. (term-size(mkterm(f;bts)) - term-size(s)) ≤ n
8. s << mkterm(f;bts)
9. r : term(opr)
10. s < r
11. r << mkterm(f;bts)
⊢ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))
BY
{ (FLemma `immediate-subterm-size` [-2] THENA Auto) }

1
1. [opr] : Type
2. f : opr
3. bts : bound-term(opr) List
4. n : ℕ
5. ∀n:ℕn. ∀s:term(opr).
     (((term-size(mkterm(f;bts)) - term-size(s)) ≤ n)
     ⇒ s << mkterm(f;bts)
     ⇒ (∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))))
6. s : term(opr)
7. (term-size(mkterm(f;bts)) - term-size(s)) ≤ n
8. s << mkterm(f;bts)
9. r : term(opr)
10. s < r
11. r << mkterm(f;bts)
12. term-size(s) < term-size(r)
⊢ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  f  :  opr
3.  bts  :  bound-term(opr)  List
4.  n  :  \mBbbN{}
5.  \mforall{}n:\mBbbN{}n.  \mforall{}s:term(opr).
          (((term-size(mkterm(f;bts))  -  term-size(s))  \mleq{}  n)
          {}\mRightarrow{}  s  <<  mkterm(f;bts)
          {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||bts||.  ((s  =  (snd(bts[i])))  \mvee{}  s  <<  snd(bts[i]))))
6.  s  :  term(opr)
7.  (term-size(mkterm(f;bts))  -  term-size(s))  \mleq{}  n
8.  s  <<  mkterm(f;bts)
9.  r  :  term(opr)
10.  s  <  r
11.  r  <<  mkterm(f;bts)
\mvdash{}  \mexists{}i:\mBbbN{}||bts||.  ((s  =  (snd(bts[i])))  \mvee{}  s  <<  snd(bts[i]))


By

---

Latex:
(FLemma  `immediate-subterm-size`  [-2]  THENA  Auto)

---

Home Index