---

Step * of Lemma bound-terms-accum_wf

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[Param:Type]. ∀[C:Param ⟶ (varname() List × hered-term(opr;t.P[t])) ⟶ Type].
∀[bts:(varname() List × hered-term(opr;t.P[t])) List].
∀[f:very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])]. ∀[g:a:Param
                                                                                   ⟶ bt:{bt:varname() List
                                                                                          × hered-term(opr;t.P[t])| 
                                                                                          (bt ∈ bts)} 
                                                                                   ⟶ C[a;bt]].
  (bound-terms-accum(L,bt.f[L;bt];a,bt.g[a;bt];bts)
   ∈ {L:(a:Param × b:varname() List × hered-term(opr;t.P[t]) × C[a;b]) List| 
      vdf-eq(Param;f;L) ∧ (map(λx.(fst(snd(x)));L) = bts ∈ ((varname() List × hered-term(opr;t.P[t])) List))} )
BY
{ (ProveWfLemma
   THEN InstLemma `dep-accum_wf` [⌜Param⌝;⌜{bt:varname() List × hered-term(opr;t.P[t])| (bt ∈ bts)} ⌝;⌜C⌝;⌜f⌝;⌜g⌝;⌜bts⌝]\000C⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[P:term(opr)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Param:Type].  \mforall{}[C:Param
                                                                                                          {}\mrightarrow{}  (varname()  List  \mtimes{}  hered-term(opr;t.P[t]))
                                                                                                          {}\mrightarrow{}  Type].
\mforall{}[bts:(varname()  List  \mtimes{}  hered-term(opr;t.P[t]))  List].
\mforall{}[f:very-dep-fun(Param;varname()  List  \mtimes{}  hered-term(opr;t.P[t]);a,bt.C[a;bt])].
\mforall{}[g:a:Param  {}\mrightarrow{}  bt:\{bt:varname()  List  \mtimes{}  hered-term(opr;t.P[t])|  (bt  \mmember{}  bts)\}    {}\mrightarrow{}  C[a;bt]].
    (bound-terms-accum(L,bt.f[L;bt];a,bt.g[a;bt];bts)  \mmember{}  \{L:(a:Param
                                                                                                              \mtimes{}  b:varname()  List  \mtimes{}  hered-term(opr;t.P[t])
                                                                                                              \mtimes{}  C[a;b])  List| 
                                                                                                              vdf-eq(Param;f;L)
                                                                                                              \mwedge{}  (map(\mlambda{}x.(fst(snd(x)));L)  =  bts)\}  )


By

---

Latex:
(ProveWfLemma
  THEN  InstLemma  `dep-accum\_wf`  [\mkleeneopen{}Param\mkleeneclose{};\mkleeneopen{}\{bt:varname()  List  \mtimes{}  hered-term(opr;t.P[t])|  (bt  \mmember{}  bts)\}  \mkleeneclose{};
  \mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}bts\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index