---

Step * of Lemma term-accum_wf

No Annotations
∀[opr,P:Type]. ∀[R:P ⟶ term(opr) ⟶ ℙ]. ∀[Q:P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P].
∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ R[p;varterm(v)]].
∀[mktermcase:p:P
             ⟶ f:opr
             ⟶ bts:(bound-term(opr) List)
             ⟶ L:{L:(t:term(opr) × p:P × R[p;t]) List| 
                   (||L|| = ||bts|| ∈ ℤ)
                   ∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
                   ∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))} 
             ⟶ R[p;mkterm(f;bts)]]. ∀[t:term(opr)]. ∀[p:P].
  (term-accum(t with p)
   p,f,vs,tr.Q[p;f;vs;tr]
   varterm(x) with p ⇒ varcase[p;x]
   mkterm(f,bts) with p ⇒ trs.mktermcase[p;f;bts;trs] ∈ R[p;t])
BY
{ (InstLemma `term-accum1_wf` [] THEN RepeatFor 7 (ParallelLast') THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr,P:Type].  \mforall{}[R:P  {}\mrightarrow{}  term(opr)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:P
                                                                                          {}\mrightarrow{}  opr
                                                                                          {}\mrightarrow{}  (varname()  List)
                                                                                          {}\mrightarrow{}  ((t:term(opr)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List)
                                                                                          {}\mrightarrow{}  P].  \mforall{}[varcase:p:P
                                                                                                                            {}\mrightarrow{}  v:\{v:varname()|  \mneg{}(v  =  nullvar())\} 
                                                                                                                            {}\mrightarrow{}  R[p;varterm(v)]].
\mforall{}[mktermcase:p:P
                          {}\mrightarrow{}  f:opr
                          {}\mrightarrow{}  bts:(bound-term(opr)  List)
                          {}\mrightarrow{}  L:\{L:(t:term(opr)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List| 
                                      (||L||  =  ||bts||)
                                      \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  ((fst(L[i]))  =  (snd(bts[i]))))
                                      \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  ((fst(snd(L[i])))  =  Q[p;f;fst(bts[i]);firstn(i;L)]))\} 
                          {}\mrightarrow{}  R[p;mkterm(f;bts)]].  \mforall{}[t:term(opr)].  \mforall{}[p:P].
    (term-accum(t  with  p)
      p,f,vs,tr.Q[p;f;vs;tr]
      varterm(x)  with  p  {}\mRightarrow{}  varcase[p;x]
      mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase[p;f;bts;trs]  \mmember{}  R[p;t])


By

---

Latex:
(InstLemma  `term-accum1\_wf`  []  THEN  RepeatFor  7  (ParallelLast')  THEN  ProveWfLemma)

---

Home Index