---

Step * of Lemma wfterm-accum_wf

No Annotations
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[Param:Type]. ∀[C:Param
                                                                                        ⟶ wfterm(opr;sort;arity)
                                                                                        ⟶ Type].
∀[nextp:Param
        ⟶ (varname() List)
        ⟶ opr
        ⟶ very-dep-fun(Param;varname() List × wfterm(opr;sort;arity);a,bt.C[a;snd(bt)])].
∀[m:a:Param
    ⟶ vs:(varname() List)
    ⟶ f:opr
    ⟶ L:{L:(a:Param × bt:varname() List × wfterm(opr;sort;arity) × C[a;snd(bt)]) List| 
          vdf-eq(Param;nextp a vs f;L) ∧ (↑wf-term(arity;sort;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())} 
                                                          ⟶ C[a;varterm(v)]]. ∀[p:Param]. ∀[t:wfterm(opr;sort;arity)].
  (wfterm-accum(p;t)
   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] ∈ C[p;t])
BY
{ (InstLemma `wfterm-hered-correct-sort-arity` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (InstLemma `hered-term-accum_wf2` [⌜opr⌝;⌜λ2t.correct-sort-arity(sort;arity;t)⌝]⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast')
   THEN Fold `wfterm-accum` (-1)
   THEN Intros
   THEN BackThruSomeHyp
   THEN MemTypeCD
   THEN EAuto 1) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[sort:term(opr)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)].  \mforall{}[Param:Type].
\mforall{}[C:Param  {}\mrightarrow{}  wfterm(opr;sort;arity)  {}\mrightarrow{}  Type].  \mforall{}[nextp:Param
                                                                                                            {}\mrightarrow{}  (varname()  List)
                                                                                                            {}\mrightarrow{}  opr
                                                                                                            {}\mrightarrow{}  very-dep-fun(Param;varname()  List
                                                                                                                  \mtimes{}  wfterm(opr;sort;arity);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{}  wfterm(opr;sort;arity)  \mtimes{}  C[a;snd(bt)])  List| 
                    vdf-eq(Param;nextp  a  vs  f;L)  \mwedge{}  (\muparrow{}wf-term(arity;sort;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())\} 
                                                                                                                    {}\mrightarrow{}  C[a;varterm(v)]].  \mforall{}[p:Param].
\mforall{}[t:wfterm(opr;sort;arity)].
    (wfterm-accum(p;t)
      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]  \mmember{}  C[p;t])


By

---

Latex:
(InstLemma  `wfterm-hered-correct-sort-arity`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (InstLemma  `hered-term-accum\_wf2`  [\mkleeneopen{}opr\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t.correct-sort-arity(sort;arity;t)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Fold  `wfterm-accum`  (-1)
  THEN  Intros
  THEN  BackThruSomeHyp
  THEN  MemTypeCD
  THEN  EAuto  1)

---

Home Index