Step
*
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. s < mkterm(f;bts)
⊢ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))
BY
{ (D -1
   THEN ExRepD
   THEN (Enough to prove bts@0 = bts ∈ (bound-term(opr) List)
          Because ((Assert ||bts@0|| = ||bts|| ∈ ℤ BY (EqCD THEN Auto)) THEN D 0 With ⌜i⌝  THEN 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. 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)
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.  s  <  mkterm(f;bts)
\mvdash{}  \mexists{}i:\mBbbN{}||bts||.  ((s  =  (snd(bts[i])))  \mvee{}  s  <<  snd(bts[i]))
By
Latex:
(D  -1
  THEN  ExRepD
  THEN  (Enough  to  prove  bts@0  =  bts
                Because  ((Assert  ||bts@0||  =  ||bts||  BY  (EqCD  THEN  Auto))  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{}    THEN  Auto)))
Home
Index