Step
*
1
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|| ∈ ℤ
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)
BY
{ (RepeatFor 2 (D -1)
THEN (Assert (fst(L[i])) = (snd(bts[i])) ∈ term(opr) BY
Auto)
THEN (RWO "-2<" (-1) THENA Auto)
THEN Reduce -1) }
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. i : ℕ
24. i < ||L||
25. <t1, x1> = L[i] ∈ (t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t))
26. t1 = (snd(bts[i])) ∈ term(opr)
⊢ ↑wf-term(arity;sort;t1)
Latex:
Latex:
1. opr : Type
2. P : Type
3. sort : \mforall{}:term(opr). \mBbbN{}
4. arity : \mforall{}:opr. ((\mBbbN{} \mtimes{} \mBbbN{}) List)
5. R : \mforall{}:P. \mforall{}:wfterm(opr;sort;arity). \mBbbP{}
6. Q : \mforall{}:P. \mforall{}:opr. \mforall{}:varname() List.
\mforall{}:(t:term(opr) \mtimes{} p:P \mtimes{} R p t supposing \muparrow{}wf-term(arity;sort;t)) List.
P
7. varcase : \mforall{}p:P. \mforall{}v:\{v:varname()| \mneg{}(v = nullvar())\} . (R p varterm(v))
8. \mforall{}[mktermcase:\mforall{}p:P. \mforall{}f:opr. \mforall{}bts:bound-term(opr) List.
\mforall{}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))))\} .
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 : \mforall{}p:P. \mforall{}f:opr. \mforall{}bts:wf-bound-terms(opr;sort;arity;f).
\mforall{}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))))\} .
(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||
17. \mforall{}i:\mBbbN{}||L||. ((fst(L[i])) = (snd(bts[i])))
18. \mforall{}i:\mBbbN{}||L||. ((fst(snd(L[i]))) = (Q p1 f (fst(bts[i])) firstn(i;L)))
19. \muparrow{}wf-term(arity;sort;mkterm(f;bts))
20. L = L
21. t1 : term(opr)
22. x1 : p:P \mtimes{} R p t1 supposing \muparrow{}wf-term(arity;sort;t1)
23. (<t1, x1> \mmember{} L)
\mvdash{} \muparrow{}wf-term(arity;sort;t1)
By
Latex:
(RepeatFor 2 (D -1)
THEN (Assert (fst(L[i])) = (snd(bts[i])) BY
Auto)
THEN (RWO "-2<" (-1) THENA Auto)
THEN Reduce -1)
Home
Index