Step
*
of Lemma
term-accum_wf_wfterm
No Annotations
∀[opr,P:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[R:P ⟶ wfterm(opr;sort;arity) ⟶ ℙ].
∀[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]. ∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ R[p;varterm(v)]].
∀[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)]]. ∀[t:wfterm(opr;sort;arity)]. ∀[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])
BY
{ (InstLemma `term-accum_wf` []
THEN RepeatFor 2 (ParallelLast')
THEN RepeatFor 3 (Intro)
THEN (D 3 With ⌜λp,t. R[p;t] supposing ↑wf-term(arity;sort;t)⌝ THENA Auto)
THEN All (RepUR ``so_apply``)
THEN Intros
THEN (Unhide
ORELSE (Auto THEN DVar `bts' THEN MemTypeCD THEN Auto THEN RWW "length_firstn select-firstn -5" 0 THEN Auto)
)
THEN (Assert ∀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]))))) BY
Auto)
THEN RenameVar `ok' (-1)
THEN (Assert ∀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]))))) BY
(Intros THEN (GenConclTerm ⌜ok f vs L⌝⋅ THENA Auto) THEN (D -2 THEN Reduce 0) THEN 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].
∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ R p varterm(v) supposing True].
∀[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))
7. 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
8. varcase : p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ (R p varterm(v))
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. 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])))))
13. ∀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])))))
⊢ 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
Latex:
Latex:
No Annotations
\mforall{}[opr,P:Type]. \mforall{}[sort:term(opr) {}\mrightarrow{} \mBbbN{}]. \mforall{}[arity:opr {}\mrightarrow{} ((\mBbbN{} \mtimes{} \mBbbN{}) List)]. \mforall{}[R:P
{}\mrightarrow{} wfterm(opr;sort;arity)
{}\mrightarrow{} \mBbbP{}].
\mforall{}[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]. \mforall{}[varcase:p:P {}\mrightarrow{} v:\{v:varname()| \mneg{}(v = nullvar())\} {}\mrightarrow{} R[p;varterm(v)]].
\mforall{}[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)]]. \mforall{}[t:wfterm(opr;sort;arity)]. \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])
By
Latex:
(InstLemma `term-accum\_wf` []
THEN RepeatFor 2 (ParallelLast')
THEN RepeatFor 3 (Intro)
THEN (D 3 With \mkleeneopen{}\mlambda{}p,t. R[p;t] supposing \muparrow{}wf-term(arity;sort;t)\mkleeneclose{} THENA Auto)
THEN All (RepUR ``so\_apply``)
THEN Intros
THEN (Unhide
ORELSE (Auto
THEN DVar `bts'
THEN MemTypeCD
THEN Auto
THEN RWW "length\_firstn select-firstn -5" 0
THEN Auto)
)
THEN (Assert \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]))))) BY
Auto)
THEN RenameVar `ok' (-1)
THEN (Assert \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]))))) BY
(Intros
THEN (GenConclTerm \mkleeneopen{}ok f vs L\mkleeneclose{}\mcdot{} THENA Auto)
THEN (D -2 THEN Reduce 0)
THEN Auto)))
Home
Index