---

Step * 1 of Lemma subterm-mkterm


1. [opr] : Type
2. s : term(opr)
3. f : opr
4. bts : bound-term(opr) List
5. s << mkterm(f;bts)
⊢ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))
BY
{ ((Enough to prove ∀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]))))
     Because (InstHyp [⌜term-size(mkterm(f;bts)) - term-size(s)⌝;⌜s⌝] (-1)⋅
              THEN Auto
              THEN FLemma `subterm-size` [-2]
              THEN Auto))
   THEN ThinVar `s'
   THEN CompleteInductionOnNat
   THEN Auto
   THEN (FLemma `subterm-cases` [-1] THENA Auto)
   THEN D -1) }

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. s < mkterm(f;bts)
⊢ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))

2
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). (s < r ∧ r << mkterm(f;bts))
⊢ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  s  :  term(opr)
3.  f  :  opr
4.  bts  :  bound-term(opr)  List
5.  s  <<  mkterm(f;bts)
\mvdash{}  \mexists{}i:\mBbbN{}||bts||.  ((s  =  (snd(bts[i])))  \mvee{}  s  <<  snd(bts[i]))


By

---

Latex:
((Enough  to  prove  \mforall{}n:\mBbbN{}.  \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]))))
      Because  (InstHyp  [\mkleeneopen{}term-size(mkterm(f;bts))  -  term-size(s)\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]  (-1)\mcdot{}
                        THEN  Auto
                        THEN  FLemma  `subterm-size`  [-2]
                        THEN  Auto))
  THEN  ThinVar  `s'
  THEN  CompleteInductionOnNat
  THEN  Auto
  THEN  (FLemma  `subterm-cases`  [-1]  THENA  Auto)
  THEN  D  -1)

---

Home Index