---

Step * 1 4 3 1 2 1 1 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
⟶ 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))
9. t : wfterm(opr;sort;arity)
10. p : P
11. 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])))))
12. ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
      (↑isl(ok f vs L)
      ⇐⇒ ||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. QQ : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P
14. (λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi )
= QQ
∈ (P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P)
15. n : ℕ
16. ∀n:ℕn. ∀a:{a:wfterm(opr;sort;arity)| term-size(a) ≤ n} .
      (λp.Ax ∈ ∀p:P
                 (term-accum(a with p)
                  p,f,vs,trs.(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs trs
                  varterm(x) with p ⇒ varcase p x
                  mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs ~ term-accum(a with p)
                                                                       p,f,vs,trs.Q p f vs trs
                                                                       varterm(x) with p ⇒ varcase p x
                                                                       mkterm(f,bts) with p ⇒ trs.mktermcase p f bts 
                                                                                                   trs))
17. term(opr) ≡ coterm-fun(opr;term(opr))
18. f : opr
19. bts : (varname() List × term(opr)) List
20. t ∈ term(opr)
21. ↑wf-term(arity;sort;mkterm(f;bts))
22. (1 + Σ(term-size(snd(bt)) | bt ∈ wfbts(mkterm(f;bts)))) ≤ n
23. mkterm(f;bts) ∈ wfterm(opr;sort;arity)
24. 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ wfbts(mkterm(f;bts))))
25. ∀bt:varname() List × wfterm(opr;sort;arity)
      ((bt ∈ wfbts(mkterm(f;bts))) ⇒ (snd(bt) ∈ {a:wfterm(opr;sort;arity)| term-size(a) ≤ (n - 1)} ))
26. ∀bt:varname() List × wfterm(opr;sort;arity)
      ((bt ∈ wfbts(mkterm(f;bts)))
      ⇒ (λp.Ax ∈ ∀p:P
                    (term-accum(snd(bt) with p)
                     p,f,vs,trs.(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs trs
                     varterm(x) with p ⇒ varcase p x
                     mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs 
                    ~ term-accum(snd(bt) with p)
                      p,f,vs,trs.Q p f vs trs
                      varterm(x) with p ⇒ varcase p x
                      mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs)))
27. p1 : P
⊢ accumulate (with value trs and list item bt):
   let p' = if isl(ok f (fst(bt)) trs) then Q p1 f (fst(bt)) trs else p1 fi  in
       trs
       @ [<snd(bt)
          , p'
          , term-accum(snd(bt) with p')
            p,f,vs,trs.if isl(ok f vs trs) then Q p f vs trs else p fi 
            varterm(x) with p ⇒ varcase p x
            mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs>]
  over list:
    wfbts(mkterm(f;bts))
  with starting value:
   []) ~ accumulate (with value trs and list item bt):
          let p' = Q p1 f (fst(bt)) trs in
              trs
              @ [<snd(bt)
                 , p'
                 , term-accum(snd(bt) with p')
                   p,f,vs,trs.Q p f vs trs
                   varterm(x) with p ⇒ varcase p x
                   mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs>]
         over list:
           wfbts(mkterm(f;bts))
         with starting value:
          [])
BY
{ ((GenConclTerm ⌜wfbts(mkterm(f;bts))⌝⋅ THENA Auto)
   THEN (Assert ∀bt:varname() List × wfterm(opr;sort;arity)
                  ((bt ∈ v)
                  ⇒ (∀p:P
                        (term-accum(snd(bt) with p)
                         p,f,vs,trs.if isl(ok f vs trs) then Q p f vs trs else p fi 
                         varterm(x) with p ⇒ varcase p x
                         mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs 
                        ~ term-accum(snd(bt) with p)
                          p,f,vs,trs.Q p f vs trs
                          varterm(x) with p ⇒ varcase p x
                          mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs))) BY
               (ParallelOp -4 THEN (ParallelLast THENA Auto) THEN UseWitness ⌜λp.Ax⌝⋅ THEN Auto))
   THEN Thin (-5)) }

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))
9. t : wfterm(opr;sort;arity)
10. p : P
11. 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])))))
12. ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
      (↑isl(ok f vs L)
      ⇐⇒ ||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. QQ : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P
14. (λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi )
= QQ
∈ (P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P)
15. n : ℕ
16. ∀n:ℕn. ∀a:{a:wfterm(opr;sort;arity)| term-size(a) ≤ n} .
      (λp.Ax ∈ ∀p:P
                 (term-accum(a with p)
                  p,f,vs,trs.(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs trs
                  varterm(x) with p ⇒ varcase p x
                  mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs ~ term-accum(a with p)
                                                                       p,f,vs,trs.Q p f vs trs
                                                                       varterm(x) with p ⇒ varcase p x
                                                                       mkterm(f,bts) with p ⇒ trs.mktermcase p f bts 
                                                                                                   trs))
17. term(opr) ≡ coterm-fun(opr;term(opr))
18. f : opr
19. bts : (varname() List × term(opr)) List
20. t ∈ term(opr)
21. ↑wf-term(arity;sort;mkterm(f;bts))
22. (1 + Σ(term-size(snd(bt)) | bt ∈ wfbts(mkterm(f;bts)))) ≤ n
23. mkterm(f;bts) ∈ wfterm(opr;sort;arity)
24. 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ wfbts(mkterm(f;bts))))
25. ∀bt:varname() List × wfterm(opr;sort;arity)
      ((bt ∈ wfbts(mkterm(f;bts))) ⇒ (snd(bt) ∈ {a:wfterm(opr;sort;arity)| term-size(a) ≤ (n - 1)} ))
26. p1 : P
27. v : wf-bound-terms(opr;sort;arity;term-opr(mkterm(f;bts)))
28. wfbts(mkterm(f;bts)) = v ∈ wf-bound-terms(opr;sort;arity;term-opr(mkterm(f;bts)))
29. ∀bt:varname() List × wfterm(opr;sort;arity)
      ((bt ∈ v)
      ⇒ (∀p:P
            (term-accum(snd(bt) with p)
             p,f,vs,trs.if isl(ok f vs trs) then Q p f vs trs else p fi 
             varterm(x) with p ⇒ varcase p x
             mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs ~ term-accum(snd(bt) with p)
                                                                  p,f,vs,trs.Q p f vs trs
                                                                  varterm(x) with p ⇒ varcase p x
                                                                  mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs)))
⊢ accumulate (with value trs and list item bt):
   let p' = if isl(ok f (fst(bt)) trs) then Q p1 f (fst(bt)) trs else p1 fi  in
       trs
       @ [<snd(bt)
          , p'
          , term-accum(snd(bt) with p')
            p,f,vs,trs.if isl(ok f vs trs) then Q p f vs trs else p fi 
            varterm(x) with p ⇒ varcase p x
            mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs>]
  over list:
    v
  with starting value:
   []) ~ accumulate (with value trs and list item bt):
          let p' = Q p1 f (fst(bt)) trs in
              trs
              @ [<snd(bt)
                 , p'
                 , term-accum(snd(bt) with p')
                   p,f,vs,trs.Q p f vs trs
                   varterm(x) with p ⇒ varcase p x
                   mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs>]
         over list:
           v
         with starting value:
          [])

---

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  :  p:P  {}\mrightarrow{}  v:\{v:varname()|  \mneg{}(v  =  nullvar())\}    {}\mrightarrow{}  (R  p  varterm(v))
8.  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))
9.  t  :  wfterm(opr;sort;arity)
10.  p  :  P
11.  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])))))
12.  \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.
            (\muparrow{}isl(ok  f  vs  L)
            \mLeftarrow{}{}\mRightarrow{}  ||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.  QQ  :  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
14.  (\mlambda{}p,f,vs,L.  if  isl(ok  f  vs  L)  then  Q  p  f  vs  L  else  p  fi  )  =  QQ
15.  n  :  \mBbbN{}
16.  \mforall{}n:\mBbbN{}n.  \mforall{}a:\{a:wfterm(opr;sort;arity)|  term-size(a)  \mleq{}  n\}  .
            (\mlambda{}p.Ax  \mmember{}  \mforall{}p:P
                                  (term-accum(a  with  p)
                                    p,f,vs,trs.(\mlambda{}p,f,vs,L.  if  isl(ok  f  vs  L)  then  Q  p  f  vs  L  else  p  fi  )  p  f  vs  trs
                                    varterm(x)  with  p  {}\mRightarrow{}  varcase  p  x
                                    mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase  p  f  bts  trs 
                                  \msim{}  term-accum(a  with  p)
                                      p,f,vs,trs.Q  p  f  vs  trs
                                      varterm(x)  with  p  {}\mRightarrow{}  varcase  p  x
                                      mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase  p  f  bts  trs))
17.  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))
18.  f  :  opr
19.  bts  :  (varname()  List  \mtimes{}  term(opr))  List
20.  t  \mmember{}  term(opr)
21.  \muparrow{}wf-term(arity;sort;mkterm(f;bts))
22.  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  wfbts(mkterm(f;bts))))  \mleq{}  n
23.  mkterm(f;bts)  \mmember{}  wfterm(opr;sort;arity)
24.  1  \mleq{}  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  wfbts(mkterm(f;bts))))
25.  \mforall{}bt:varname()  List  \mtimes{}  wfterm(opr;sort;arity)
            ((bt  \mmember{}  wfbts(mkterm(f;bts)))  {}\mRightarrow{}  (snd(bt)  \mmember{}  \{a:wfterm(opr;sort;arity)|  term-size(a)  \mleq{}  (n  -  1)\}  \000C))
26.  \mforall{}bt:varname()  List  \mtimes{}  wfterm(opr;sort;arity)
            ((bt  \mmember{}  wfbts(mkterm(f;bts)))
            {}\mRightarrow{}  (\mlambda{}p.Ax  \mmember{}  \mforall{}p:P
                                        (term-accum(snd(bt)  with  p)
                                          p,f,vs,trs.(\mlambda{}p,f,vs,L.  if  isl(ok  f  vs  L)  then  Q  p  f  vs  L  else  p  fi  )  p  f  vs  trs
                                          varterm(x)  with  p  {}\mRightarrow{}  varcase  p  x
                                          mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase  p  f  bts  trs 
                                        \msim{}  term-accum(snd(bt)  with  p)
                                            p,f,vs,trs.Q  p  f  vs  trs
                                            varterm(x)  with  p  {}\mRightarrow{}  varcase  p  x
                                            mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase  p  f  bts  trs)))
27.  p1  :  P
\mvdash{}  accumulate  (with  value  trs  and  list  item  bt):
      let  p'  =  if  isl(ok  f  (fst(bt))  trs)  then  Q  p1  f  (fst(bt))  trs  else  p1  fi    in
              trs
              @  [<snd(bt)
                    ,  p'
                    ,  term-accum(snd(bt)  with  p')
                        p,f,vs,trs.if  isl(ok  f  vs  trs)  then  Q  p  f  vs  trs  else  p  fi 
                        varterm(x)  with  p  {}\mRightarrow{}  varcase  p  x
                        mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase  p  f  bts  trs>]
    over  list:
        wfbts(mkterm(f;bts))
    with  starting  value:
      [])  \msim{}  accumulate  (with  value  trs  and  list  item  bt):
                    let  p'  =  Q  p1  f  (fst(bt))  trs  in
                            trs
                            @  [<snd(bt)
                                  ,  p'
                                  ,  term-accum(snd(bt)  with  p')
                                      p,f,vs,trs.Q  p  f  vs  trs
                                      varterm(x)  with  p  {}\mRightarrow{}  varcase  p  x
                                      mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase  p  f  bts  trs>]
                  over  list:
                      wfbts(mkterm(f;bts))
                  with  starting  value:
                    [])


By

---

Latex:
((GenConclTerm  \mkleeneopen{}wfbts(mkterm(f;bts))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mforall{}bt:varname()  List  \mtimes{}  wfterm(opr;sort;arity)
                                ((bt  \mmember{}  v)
                                {}\mRightarrow{}  (\mforall{}p:P
                                            (term-accum(snd(bt)  with  p)
                                              p,f,vs,trs.if  isl(ok  f  vs  trs)  then  Q  p  f  vs  trs  else  p  fi 
                                              varterm(x)  with  p  {}\mRightarrow{}  varcase  p  x
                                              mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase  p  f  bts  trs 
                                            \msim{}  term-accum(snd(bt)  with  p)
                                                p,f,vs,trs.Q  p  f  vs  trs
                                                varterm(x)  with  p  {}\mRightarrow{}  varcase  p  x
                                                mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase  p  f  bts  trs)))  BY
                          (ParallelOp  -4  THEN  (ParallelLast  THENA  Auto)  THEN  UseWitness  \mkleeneopen{}\mlambda{}p.Ax\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Thin  (-5))

---

Home Index