---

Step * 1 of Lemma term-accum_wf_wfterm_0


1. opr : Type
2. P : Type
3. sort : term(opr) ⟶ ℕ
4. arity : opr ⟶ ((ℕ × ℕ) List)
5. R : P ⟶ wfterm(opr;sort;arity) ⟶ ℙ
6. Q : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P
7. varcase : p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ (R p varterm(v))
8. ∀[mktermcase:p:P
                ⟶ f:opr
                ⟶ bts:(bound-term(opr) List)
                ⟶ L:{L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;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) supposing ↑wf-term(arity;sort;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 supposing ↑wf-term(arity;sort;t))
9. 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))
10. t : wfterm(opr;sort;arity)
11. p : P
12. p1 : P
13. f : opr
14. bts : bound-term(opr) List
15. L : {L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List| 
         (||L|| = ||bts|| ∈ ℤ)
         ∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
         ∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = (Q p1 f (fst(bts[i])) firstn(i;L)) ∈ P))} 
16. ↑wf-term(arity;sort;mkterm(f;bts))
⊢ mktermcase p1 f bts L ∈ R p1 mkterm(f;bts)
BY
{ (Enough to prove L ∈ {L:(t:wfterm(opr;sort;arity) × p:P × (R p t)) List| 
                        (||L|| = ||wfbts(mkterm(f;bts))|| ∈ ℤ)
                        ∧ (i:ℕ||L|| ⟶ ((fst(L[i])) = (snd(wfbts(mkterm(f;bts))[i])) ∈ term(opr)))
                        ∧ (i:ℕ||L|| ⟶ ((fst(snd(L[i]))) = (Q p1 f (fst(wfbts(mkterm(f;bts))[i])) firstn(i;L)) ∈ P))} 
    Because ((Assert mkterm(f;bts) ∈ wfterm(opr;sort;arity) BY
                    (MemTypeCD THEN Auto))
             THEN (Subst' bts ~ wfbts(mkterm(f;bts)) 0 THENA Computation)
             THEN (Subst' bts ~ wfbts(mkterm(f;bts)) -4 THENA Computation)
             THEN All (RepUR ``all``)
             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 ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P
7. varcase : p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ (R p varterm(v))
8. ∀[mktermcase:p:P
                ⟶ f:opr
                ⟶ bts:(bound-term(opr) List)
                ⟶ L:{L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;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) supposing ↑wf-term(arity;sort;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 supposing ↑wf-term(arity;sort;t))
9. 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))
10. t : wfterm(opr;sort;arity)
11. p : P
12. p1 : P
13. f : opr
14. bts : bound-term(opr) List
15. L : {L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List| 
         (||L|| = ||bts|| ∈ ℤ)
         ∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
         ∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = (Q p1 f (fst(bts[i])) firstn(i;L)) ∈ P))} 
16. ↑wf-term(arity;sort;mkterm(f;bts))
⊢ L ∈ {L:(t:wfterm(opr;sort;arity) × p:P × (R p t)) List| 
       (||L|| = ||wfbts(mkterm(f;bts))|| ∈ ℤ)
       ∧ (i:ℕ||L|| ⟶ ((fst(L[i])) = (snd(wfbts(mkterm(f;bts))[i])) ∈ term(opr)))
       ∧ (i:ℕ||L|| ⟶ ((fst(snd(L[i]))) = (Q p1 f (fst(wfbts(mkterm(f;bts))[i])) firstn(i;L)) ∈ P))} 

---

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{}  opr
{}\mrightarrow{}  (varname()  List)
{}\mrightarrow{}  ((t:term(opr)  \mtimes{}  p:P  \mtimes{}  R  p  t  supposing  \muparrow{}wf-term(arity;sort;t))  List)
{}\mrightarrow{}  P
7.  varcase  :  p:P  {}\mrightarrow{}  v:\{v:varname()|  \mneg{}(v  =  nullvar())\}    {}\mrightarrow{}  (R  p  varterm(v))
8.  \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  supposing  \muparrow{}wf-term(arity;sort;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)  supposing  \muparrow{}wf-term(arity;sort;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  supposing  \muparrow{}wf-term(arity;sort;t))
9.  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))
10.  t  :  wfterm(opr;sort;arity)
11.  p  :  P
12.  p1  :  P
13.  f  :  opr
14.  bts  :  bound-term(opr)  List
15.  L  :  \{L:(t:term(opr)  \mtimes{}  p:P  \mtimes{}  R  p  t  supposing  \muparrow{}wf-term(arity;sort;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  p1  f  (fst(bts[i]))  firstn(i;L))))\} 
16.  \muparrow{}wf-term(arity;sort;mkterm(f;bts))
\mvdash{}  mktermcase  p1  f  bts  L  \mmember{}  R  p1  mkterm(f;bts)


By

---

Latex:
(Enough  to  prove  L  \mmember{}  \{L:(t:wfterm(opr;sort;arity)  \mtimes{}  p:P  \mtimes{}  (R  p  t))  List| 
                                            (||L||  =  ||wfbts(mkterm(f;bts))||)
                                            \mwedge{}  (i:\mBbbN{}||L||  {}\mrightarrow{}  ((fst(L[i]))  =  (snd(wfbts(mkterm(f;bts))[i]))))
                                            \mwedge{}  (i:\mBbbN{}||L||  {}\mrightarrow{}  ((fst(snd(L[i])))
                                                                          =  (Q  p1  f  (fst(wfbts(mkterm(f;bts))[i]))  firstn(i;L))))\} 
    Because  ((Assert  mkterm(f;bts)  \mmember{}  wfterm(opr;sort;arity)  BY
                                    (MemTypeCD  THEN  Auto))
                      THEN  (Subst'  bts  \msim{}  wfbts(mkterm(f;bts))  0  THENA  Computation)
                      THEN  (Subst'  bts  \msim{}  wfbts(mkterm(f;bts))  -4  THENA  Computation)
                      THEN  All  (RepUR  ``all``)
                      THEN  Auto))

---

Home Index