---

Step * 1 1 1 1 of Lemma hered-term-accum_wf


1. opr : Type
2. P : term(opr) ⟶ ℙ
3. Param : Type
4. C : Param ⟶ (varname() List × hered-term(opr;t.P[t])) ⟶ Type
5. nextp : Param ⟶ (varname() List) ⟶ opr ⟶ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])
6. m : a:Param
⟶ vs:(varname() List)
⟶ f:opr
⟶ L:{L:(a:Param × bt:varname() List × hered-term(opr;t.P[t]) × C[a;bt]) List| 
      vdf-eq(Param;nextp a vs f;L) ∧ hereditarily(opr;s.P[s];mkterm(f;map(λx.(fst(snd(x)));L)))} 
⟶ C[a;<vs, mkterm(f;map(λx.(fst(snd(x)));L))>]
7. varcase : a:Param
⟶ vs:(varname() List)
⟶ v:{v:varname()| (¬(v = nullvar() ∈ varname())) ∧ P[varterm(v)]} 
⟶ C[a;<vs, varterm(v)>]
8. n : ℕ
9. ∀n:ℕn. ∀p:Param. ∀bt:varname() List × hered-term(opr;t.P[t]).
     ((term-size(snd(bt)) ≤ n)
     ⇒ (hered-term-accum(p,vs,v.varcase[p;vs;v];
                          prm,vs,f,L.m[prm;vs;f;L];
                          p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt];
                          p;
                          bt) ∈ C[p;bt]))
10. p : Param
11. b1 : varname() List
12. y1 : opr
13. y2 : (varname() List × term(opr)) List
14. hereditarily(opr;s.P[s];inr <y1, y2> )
15. term-size(inr <y1, y2> ) ≤ n
16. λsofar,bt. nextp[p;b1;y1;sofar;bt] ∈ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])
17. y2 ∈ (varname() List × hered-term(opr;t.P[t])) List
18. a : Param
19. bt : varname() List × hered-term(opr;t.P[t])
20. (bt ∈ y2)
⊢ term-size(snd(bt)) < 1 + Σ(term-size(snd(bt)) | bt ∈ y2)
BY
{ (RepeatFor 2 (D -1)
   THEN InstLemma `summand-le-lsum` [⌜varname() List × term(opr)⌝;⌜y2⌝;⌜λ2bt.term-size(snd(bt))⌝;⌜bt⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  P  :  term(opr)  {}\mrightarrow{}  \mBbbP{}
3.  Param  :  Type
4.  C  :  Param  {}\mrightarrow{}  (varname()  List  \mtimes{}  hered-term(opr;t.P[t]))  {}\mrightarrow{}  Type
5.  nextp  :  Param
{}\mrightarrow{}  (varname()  List)
{}\mrightarrow{}  opr
{}\mrightarrow{}  very-dep-fun(Param;varname()  List  \mtimes{}  hered-term(opr;t.P[t]);a,bt.C[a;bt])
6.  m  :  a:Param
{}\mrightarrow{}  vs:(varname()  List)
{}\mrightarrow{}  f:opr
{}\mrightarrow{}  L:\{L:(a:Param  \mtimes{}  bt:varname()  List  \mtimes{}  hered-term(opr;t.P[t])  \mtimes{}  C[a;bt])  List| 
            vdf-eq(Param;nextp  a  vs  f;L)  \mwedge{}  hereditarily(opr;s.P[s];mkterm(f;map(\mlambda{}x.(fst(snd(x)));L)))\} 
{}\mrightarrow{}  C[a;<vs,  mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))>]
7.  varcase  :  a:Param
{}\mrightarrow{}  vs:(varname()  List)
{}\mrightarrow{}  v:\{v:varname()|  (\mneg{}(v  =  nullvar()))  \mwedge{}  P[varterm(v)]\} 
{}\mrightarrow{}  C[a;<vs,  varterm(v)>]
8.  n  :  \mBbbN{}
9.  \mforall{}n:\mBbbN{}n.  \mforall{}p:Param.  \mforall{}bt:varname()  List  \mtimes{}  hered-term(opr;t.P[t]).
          ((term-size(snd(bt))  \mleq{}  n)
          {}\mRightarrow{}  (hered-term-accum(p,vs,v.varcase[p;vs;v];
                                                    prm,vs,f,L.m[prm;vs;f;L];
                                                    p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt];
                                                    p;
                                                    bt)  \mmember{}  C[p;bt]))
10.  p  :  Param
11.  b1  :  varname()  List
12.  y1  :  opr
13.  y2  :  (varname()  List  \mtimes{}  term(opr))  List
14.  hereditarily(opr;s.P[s];inr  <y1,  y2>  )
15.  term-size(inr  <y1,  y2>  )  \mleq{}  n
16.  \mlambda{}sofar,bt.  nextp[p;b1;y1;sofar;bt]  \mmember{}  very-dep-fun(Param;varname()  List
        \mtimes{}  hered-term(opr;t.P[t]);a,bt.C[a;bt])
17.  y2  \mmember{}  (varname()  List  \mtimes{}  hered-term(opr;t.P[t]))  List
18.  a  :  Param
19.  bt  :  varname()  List  \mtimes{}  hered-term(opr;t.P[t])
20.  (bt  \mmember{}  y2)
\mvdash{}  term-size(snd(bt))  <  1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  y2)


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  InstLemma  `summand-le-lsum`  [\mkleeneopen{}varname()  List  \mtimes{}  term(opr)\mkleeneclose{};\mkleeneopen{}y2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}bt.term-size(snd(bt))\mkleeneclose{};\mkleeneopen{}bt\mkleeneclose{}]
  \mcdot{}
  THEN  Auto)

---

Home Index