---

Step * of Lemma wf-term-accum-induction

No Annotations
∀[opr,P:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[R:P ⟶ wfterm(opr;sort;arity) ⟶ ℙ].
  ∀Q:P
     ⟶ f:opr
     ⟶ vs:(varname() List)
     ⟶ {L:(t:wfterm(opr;sort;arity) × p:P × R[p;t]) List| 
         ||L|| < ||arity f||
         ∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
         ∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))} 
     ⟶ P
    ((∀p:P. ∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} .  R[p;varterm(v)])
    ⇒ (∀p:P. ∀f:opr. ∀bts:wf-bound-terms(opr;sort;arity;f). ∀L:{L:(t:wfterm(opr;sort;arity) × 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;mkwfterm(f;bts)])
    ⇒ (∀p:P. ∀t:wfterm(opr;sort;arity).  R[p;t]))
BY
{ (InstLemma `term-accum_wf_wfterm` []
   THEN RepeatFor 6 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN RenameVar `varcase' (-1)
   THEN (D -2 With ⌜varcase⌝  THENA Auto)
   THEN D 0
   THEN Try ((RenameVar `mktermcase' (-1)
              THEN (D -2 With ⌜mktermcase⌝  THENA Auto)
              THEN Intros
              THEN (D -3 With ⌜t⌝  THENA Auto)
              THEN (D -1 With ⌜p⌝  THENA Auto)
              THEN UseWitness ⌜term-accum(t with p)
                               p,f,vs,L.Q[p;f;vs;L]
                               varterm(x) with p ⇒ varcase[p;x]
                               mkterm(f,bts) with p ⇒ trs.mktermcase[p;f;bts;trs]⌝⋅
              THEN Auto))
   THEN Auto) }

1
1. opr : Type
2. P : Type
3. sort : term(opr) ⟶ ℕ
4. arity : opr ⟶ ((ℕ × ℕ) List)
5. R : P ⟶ wfterm(opr;sort;arity) ⟶ ℙ
6. Q : P
⟶ f:opr
⟶ vs:(varname() List)
⟶ {L:(t:wfterm(opr;sort;arity) × p:P × R[p;t]) List| 
    ||L|| < ||arity f||
    ∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
    ∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))} 
⟶ P
7. varcase : ∀p:P. ∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} .  R[p;varterm(v)]
8. ∀[mktermcase:p:P
                ⟶ f:opr
                ⟶ bts:wf-bound-terms(opr;sort;arity;f)
                ⟶ L:{L:(t:wfterm(opr;sort;arity) × 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;mkwfterm(f;bts)]]. ∀[t:wfterm(opr;sort;arity)]. ∀[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])
9. p : P
10. f : opr
11. bts : wf-bound-terms(opr;sort;arity;f)
12. L : (t:wfterm(opr;sort;arity) × p:P × R[p;t]) List
13. x : ||L|| = ||bts|| ∈ ℤ
14. x1 : ∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr))
15. i : ℕ||L||
⊢ firstn(i;L) ∈ {L:(t:wfterm(opr;sort;arity) × p:P × R[p;t]) List| 
                 ||L|| < ||arity f||
                 ∧ (||fst(bts[i])|| = (fst(arity f[||L||])) ∈ ℤ)
                 ∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr,P:Type].  \mforall{}[sort:term(opr)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)].  \mforall{}[R:P
                                                                                                                                                      {}\mrightarrow{}  wfterm(opr;sort;arity)
                                                                                                                                                      {}\mrightarrow{}  \mBbbP{}].
    \mforall{}Q:P
          {}\mrightarrow{}  f:opr
          {}\mrightarrow{}  vs:(varname()  List)
          {}\mrightarrow{}  \{L:(t:wfterm(opr;sort;arity)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List| 
                  ||L||  <  ||arity  f||
                  \mwedge{}  (||vs||  =  (fst(arity  f[||L||])))
                  \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  ((sort  (fst(L[i])))  =  (snd(arity  f[i]))))\} 
          {}\mrightarrow{}  P
        ((\mforall{}p:P.  \mforall{}v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  .    R[p;varterm(v)])
        {}\mRightarrow{}  (\mforall{}p:P.  \mforall{}f:opr.  \mforall{}bts:wf-bound-terms(opr;sort;arity;f).  \mforall{}L:\{L:(t:wfterm(opr;sort;arity)
                                                                                                                                  \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)]))\}  .
                    R[p;mkwfterm(f;bts)])
        {}\mRightarrow{}  (\mforall{}p:P.  \mforall{}t:wfterm(opr;sort;arity).    R[p;t]))


By

---

Latex:
(InstLemma  `term-accum\_wf\_wfterm`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `varcase'  (-1)
  THEN  (D  -2  With  \mkleeneopen{}varcase\mkleeneclose{}    THENA  Auto)
  THEN  D  0
  THEN  Try  ((RenameVar  `mktermcase'  (-1)
                        THEN  (D  -2  With  \mkleeneopen{}mktermcase\mkleeneclose{}    THENA  Auto)
                        THEN  Intros
                        THEN  (D  -3  With  \mkleeneopen{}t\mkleeneclose{}    THENA  Auto)
                        THEN  (D  -1  With  \mkleeneopen{}p\mkleeneclose{}    THENA  Auto)
                        THEN  UseWitness  \mkleeneopen{}term-accum(t  with  p)
                                                          p,f,vs,L.Q[p;f;vs;L]
                                                          varterm(x)  with  p  {}\mRightarrow{}  varcase[p;x]
                                                          mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase[p;f;bts;trs]\mkleeneclose{}\mcdot{}
                        THEN  Auto))
  THEN  Auto)

---

Home Index