---

Step * 1 1 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 : (t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List
16. (||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))
17. ↑wf-term(arity;sort;mkterm(f;bts))
⊢ L ∈ (t:wfterm(opr;sort;arity) × p:P × (R p t)) List
BY
{ (All (Fold `all`)
   THEN (SubsumeC ⌜{tr:t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)| (tr ∈ L)}  List⌝⋅
         THENL [Auto; RepeatFor 2 ((SubtypeReasoning1 THENA Auto))]
   )
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN D -2
   THEN (Enough to prove ↑wf-term(arity;sort;t1)
          Because 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 : (t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List
16. ||L|| = ||bts|| ∈ ℤ
17. ∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr))
18. ∀i:ℕ||L||. ((fst(snd(L[i]))) = (Q p1 f (fst(bts[i])) firstn(i;L)) ∈ P)
19. ↑wf-term(arity;sort;mkterm(f;bts))
20. L = L ∈ ({tr:t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)| (tr ∈ L)}  List)
21. t1 : term(opr)
22. x1 : p:P × R p t1 supposing ↑wf-term(arity;sort;t1)
23. (<t1, x1> ∈ L)
⊢ ↑wf-term(arity;sort;t1)

---

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  :  (t:term(opr)  \mtimes{}  p:P  \mtimes{}  R  p  t  supposing  \muparrow{}wf-term(arity;sort;t))  List
16.  (||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))))
17.  \muparrow{}wf-term(arity;sort;mkterm(f;bts))
\mvdash{}  L  \mmember{}  (t:wfterm(opr;sort;arity)  \mtimes{}  p:P  \mtimes{}  (R  p  t))  List


By

---

Latex:
(All  (Fold  `all`)
  THEN  (SubsumeC  \mkleeneopen{}\{tr:t:term(opr)  \mtimes{}  p:P  \mtimes{}  R  p  t  supposing  \muparrow{}wf-term(arity;sort;t)|  (tr  \mmember{}  L)\}    List\mkleeneclose{}\mcdot{}
              THENL  [Auto;  RepeatFor  2  ((SubtypeReasoning1  THENA  Auto))]
  )
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  D  -2
  THEN  (Enough  to  prove  \muparrow{}wf-term(arity;sort;t1)
                Because  Auto))

---

Home Index