---

Step * 1 4 3 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. x : varname()
19. [%11] : ¬(x = nullvar() ∈ varname())
20. t ∈ term(opr)
21. True
22. 1 ≤ n
⊢ λp.Ax ∈ ∀p:P. (varcase p x ~ varcase p x)
BY
{ (Reduce 0 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.  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.  x  :  varname()
19.  [\%11]  :  \mneg{}(x  =  nullvar())
20.  t  \mmember{}  term(opr)
21.  True
22.  1  \mleq{}  n
\mvdash{}  \mlambda{}p.Ax  \mmember{}  \mforall{}p:P.  (varcase  p  x  \msim{}  varcase  p  x)


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index