Step
*
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 : {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 p1 f (fst(bts[i])) firstn(i;L)) ∈ P))}
16. ↑wf-term(arity;sort;mkterm(f;bts))
⊢ L ∈ {L:(t:wfterm(opr;sort;arity) × p:P × (R p t)) List|
(||L|| = ||wfbts(mkterm(f;bts))|| ∈ ℤ)
∧ (i:ℕ||L|| ⟶ ((fst(L[i])) = (snd(wfbts(mkterm(f;bts))[i])) ∈ term(opr)))
∧ (i:ℕ||L|| ⟶ ((fst(snd(L[i]))) = (Q p1 f (fst(wfbts(mkterm(f;bts))[i])) firstn(i;L)) ∈ P))}
BY
{ (DVar `L' THEN (Subst' wfbts(mkterm(f;bts)) ~ bts 0 THENA Computation) THEN MemTypeCD THEN Try (Trivial)) }
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|| ∈ ℤ)
∧ (∀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
2
.....wf.....
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))
18. L1 : (t:wfterm(opr;sort;arity) × p:P × (R p t)) List
⊢ istype((||L1|| = ||bts|| ∈ ℤ)
∧ (i:ℕ||L1|| ⟶ ((fst(L1[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (i:ℕ||L1|| ⟶ ((fst(snd(L1[i]))) = (Q p1 f (fst(bts[i])) firstn(i;L1)) ∈ P)))
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 : \{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 p1 f (fst(bts[i])) firstn(i;L))))\}
16. \muparrow{}wf-term(arity;sort;mkterm(f;bts))
\mvdash{} L \mmember{} \{L:(t:wfterm(opr;sort;arity) \mtimes{} p:P \mtimes{} (R p t)) List|
(||L|| = ||wfbts(mkterm(f;bts))||)
\mwedge{} (i:\mBbbN{}||L|| {}\mrightarrow{} ((fst(L[i])) = (snd(wfbts(mkterm(f;bts))[i]))))
\mwedge{} (i:\mBbbN{}||L|| {}\mrightarrow{} ((fst(snd(L[i]))) = (Q p1 f (fst(wfbts(mkterm(f;bts))[i])) firstn(i;L))))\}
By
Latex:
(DVar `L'
THEN (Subst' wfbts(mkterm(f;bts)) \msim{} bts 0 THENA Computation)
THEN MemTypeCD
THEN Try (Trivial))
Home
Index