---

Step * of Lemma hered-term-accum_wf2

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[Param:Type]. ∀[C:Param ⟶ hered-term(opr;t.P[t]) ⟶ Type].
∀[nextp:Param
        ⟶ (varname() List)
        ⟶ opr
        ⟶ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;snd(bt)])].
∀[m:a:Param
    ⟶ vs:(varname() List)
    ⟶ f:opr
    ⟶ L:{L:(a:Param × bt:varname() List × hered-term(opr;t.P[t]) × C[a;snd(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;mkterm(f;map(λx.(fst(snd(x)));L))]]. ∀[varcase:a:Param
                                                          ⟶ vs:(varname() List)
                                                          ⟶ v:{v:varname()| 
                                                                (¬(v = nullvar() ∈ varname())) ∧ P[varterm(v)]} 
                                                          ⟶ C[a;varterm(v)]]. ∀[p:Param]. ∀[t:hered-term(opr;t.P[t])].
  (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;
                    <[], t>) ∈ C[p;t])
BY
{ (InstLemma `hered-term-accum_wf` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Intro
   THEN (D -2 With ⌜λ2p bt.C p (snd(bt))⌝  THENA Auto)
   THEN All (RepUR ``so_apply so_lambda``)
   THEN RepeatFor 2 (ParallelLast')
   THEN Intro
   THEN Try (((D -2 With ⌜varcase⌝  THENA Auto) THEN ParallelLast' THEN Intro THEN BHyp -2 THEN Auto))
   THEN RepeatFor 3 ((D 0 THENL [Auto; Id]))
   THEN (Assert varterm(v) ∈ hered-term(opr;t.P[t]) BY
               (DVar `v' THEN MemTypeCD))
   THEN EAuto 1) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[P:term(opr)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Param:Type].  \mforall{}[C:Param  {}\mrightarrow{}  hered-term(opr;t.P[t])  {}\mrightarrow{}  Type].
\mforall{}[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;snd(bt)])].
\mforall{}[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;snd(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;mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))]].  \mforall{}[varcase:a:Param
                                                                                                                    {}\mrightarrow{}  vs:(varname()  List)
                                                                                                                    {}\mrightarrow{}  v:\{v:varname()| 
                                                                                                                                (\mneg{}(v  =  nullvar()))  \mwedge{}  P[varterm(v)]\} 
                                                                                                                    {}\mrightarrow{}  C[a;varterm(v)]].  \mforall{}[p:Param].
\mforall{}[t:hered-term(opr;t.P[t])].
    (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;
                                        <[],  t>)  \mmember{}  C[p;t])


By

---

Latex:
(InstLemma  `hered-term-accum\_wf`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Intro
  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}\msubtwo{}p  bt.C  p  (snd(bt))\mkleeneclose{}    THENA  Auto)
  THEN  All  (RepUR  ``so\_apply  so\_lambda``)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Intro
  THEN  Try  (((D  -2  With  \mkleeneopen{}varcase\mkleeneclose{}    THENA  Auto)  THEN  ParallelLast'  THEN  Intro  THEN  BHyp  -2  THEN  Auto))
  THEN  RepeatFor  3  ((D  0  THENL  [Auto;  Id]))
  THEN  (Assert  varterm(v)  \mmember{}  hered-term(opr;t.P[t])  BY
                          (DVar  `v'  THEN  MemTypeCD))
  THEN  EAuto  1)

---

Home Index