---

Step * 1 of Lemma wf-term-accum-induction


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])) ∈ ℤ))} 
BY
{ (DVar `bts'
   THEN (MemTypeCD
         THENL [Auto
               ; (RWO "length_firstn" 0 THEN Auto THEN RWO "select-firstn" 0 THEN Auto THEN RWO "-5" 0 THEN Auto)
               ; Auto]
        )
   ) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  P  :  Type
3.  sort  :  term(opr)  {}\mrightarrow{}  \mBbbN{}
4.  arity  :  opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)
5.  R  :  P  {}\mrightarrow{}  wfterm(opr;sort;arity)  {}\mrightarrow{}  \mBbbP{}
6.  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
7.  varcase  :  \mforall{}p:P.  \mforall{}v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  .    R[p;varterm(v)]
8.  \mforall{}[mktermcase:p:P
                                {}\mrightarrow{}  f:opr
                                {}\mrightarrow{}  bts:wf-bound-terms(opr;sort;arity;f)
                                {}\mrightarrow{}  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)]))\} 
                                {}\mrightarrow{}  R[p;mkwfterm(f;bts)]].  \mforall{}[t:wfterm(opr;sort;arity)].  \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])
9.  p  :  P
10.  f  :  opr
11.  bts  :  wf-bound-terms(opr;sort;arity;f)
12.  L  :  (t:wfterm(opr;sort;arity)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List
13.  x  :  ||L||  =  ||bts||
14.  x1  :  \mforall{}i:\mBbbN{}||L||.  ((fst(L[i]))  =  (snd(bts[i])))
15.  i  :  \mBbbN{}||L||
\mvdash{}  firstn(i;L)  \mmember{}  \{L:(t:wfterm(opr;sort;arity)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List| 
                                  ||L||  <  ||arity  f||
                                  \mwedge{}  (||fst(bts[i])||  =  (fst(arity  f[||L||])))
                                  \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  ((sort  (fst(L[i])))  =  (snd(arity  f[i]))))\} 


By

---

Latex:
(DVar  `bts'
  THEN  (MemTypeCD
              THENL  [Auto
                          ;  (RWO  "length\_firstn"  0
                                THEN  Auto
                                THEN  RWO  "select-firstn"  0
                                THEN  Auto
                                THEN  RWO  "-5"  0
                                THEN  Auto)
                          ;  Auto]
            )
  )

---

Home Index