---

Step * 1 3 of Lemma term-accum_wf_wfterm


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].
   ∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ R p varterm(v) supposing True].
   ∀[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))
7. 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
8. varcase : p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ (R p varterm(v))
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. ok : ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
           Dec(||L|| < ||arity f||
           ∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
           ∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))
           ∧ (∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))))
13. p1 : P
14. f : opr
15. vs : varname() List
16. L : (t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List
17. ↑isl(ok f vs L)
18. ||L|| < ||arity f||
19. ||vs|| = (fst(arity f[||L||])) ∈ ℤ
20. ∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ)
21. ∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))
22. L = L ∈ ({x:t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)| (x ∈ L)}  List)
23. t1 : term(opr)
24. p2 : P
25. x2 : R p2 t1 supposing ↑wf-term(arity;sort;t1)
26. (<t1, p2, x2> ∈ L)
27. p3 : P
⊢ t1 ∈ wfterm(opr;sort;arity)
BY
{ (Thin (-1)
   THEN RepeatFor 2 (D -1)
   THEN (D -8 With ⌜i⌝  THENA Auto)
   THEN (RWO "-2<" (-1) THENA Auto)
   THEN Reduce -1
   THEN 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.  \mforall{}[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].  \mforall{}[varcase:p:P  {}\mrightarrow{}  v:\{v:varname()|  \mneg{}(v  =  nullvar())\}    {}\mrightarrow{}  R  p  varterm(v)  supposing  True].
      \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))
7.  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
8.  varcase  :  p:P  {}\mrightarrow{}  v:\{v:varname()|  \mneg{}(v  =  nullvar())\}    {}\mrightarrow{}  (R  p  varterm(v))
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.  ok  :  \mforall{}f:opr.  \mforall{}vs:varname()  List.
                  \mforall{}L:(t:term(opr)  \mtimes{}  p:P  \mtimes{}  R  p  t  supposing  \muparrow{}wf-term(arity;sort;t))  List.
                      Dec(||L||  <  ||arity  f||
                      \mwedge{}  (||vs||  =  (fst(arity  f[||L||])))
                      \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  ((sort  (fst(L[i])))  =  (snd(arity  f[i]))))
                      \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  (\muparrow{}wf-term(arity;sort;fst(L[i])))))
13.  p1  :  P
14.  f  :  opr
15.  vs  :  varname()  List
16.  L  :  (t:term(opr)  \mtimes{}  p:P  \mtimes{}  R  p  t  supposing  \muparrow{}wf-term(arity;sort;t))  List
17.  \muparrow{}isl(ok  f  vs  L)
18.  ||L||  <  ||arity  f||
19.  ||vs||  =  (fst(arity  f[||L||]))
20.  \mforall{}i:\mBbbN{}||L||.  ((sort  (fst(L[i])))  =  (snd(arity  f[i])))
21.  \mforall{}i:\mBbbN{}||L||.  (\muparrow{}wf-term(arity;sort;fst(L[i])))
22.  L  =  L
23.  t1  :  term(opr)
24.  p2  :  P
25.  x2  :  R  p2  t1  supposing  \muparrow{}wf-term(arity;sort;t1)
26.  (<t1,  p2,  x2>  \mmember{}  L)
27.  p3  :  P
\mvdash{}  t1  \mmember{}  wfterm(opr;sort;arity)


By

---

Latex:
(Thin  (-1)
  THEN  RepeatFor  2  (D  -1)
  THEN  (D  -8  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  (RWO  "-2<"  (-1)  THENA  Auto)
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index