---

Step * 1 1 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. f@0 : opr
10. bts@0 : bound-term(opr) List
11. mkterm(f;bts) = mkterm(f@0;bts@0) ∈ term(opr)
12. i : ℕ||bts@0||
13. s = (snd(bts@0[i])) ∈ term(opr)
⊢ bts@0 = bts ∈ (bound-term(opr) List)
BY
{ (FLemma `mkterm-one-one` [-3] THEN Auto) }

---

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.  f@0  :  opr
10.  bts@0  :  bound-term(opr)  List
11.  mkterm(f;bts)  =  mkterm(f@0;bts@0)
12.  i  :  \mBbbN{}||bts@0||
13.  s  =  (snd(bts@0[i]))
\mvdash{}  bts@0  =  bts


By

---

Latex:
(FLemma  `mkterm-one-one`  [-3]  THEN  Auto)

---

Home Index