Step
*
of Lemma
hered-term-accum_wf
No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[Param:Type]. ∀[C:Param ⟶ (varname() List × hered-term(opr;t.P[t])) ⟶ Type].
∀[nextp:Param ⟶ (varname() List) ⟶ opr ⟶ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])].
∀[m:a:Param
⟶ vs:(varname() List)
⟶ f:opr
⟶ L:{L:(a:Param × bt:varname() List × hered-term(opr;t.P[t]) × C[a;bt]) List|
vdf-eq(Param;nextp a vs f;L) ∧ hereditarily(opr;s.P[s];mkterm(f;map(λx.(fst(snd(x)));L)))}
⟶ C[a;<vs, mkterm(f;map(λx.(fst(snd(x)));L))>]]. ∀[varcase:a:Param
⟶ vs:(varname() List)
⟶ v:{v:varname()|
(¬(v = nullvar() ∈ varname())) ∧ P[varterm(v)]}
⟶ C[a;<vs, varterm(v)>]]. ∀[p:Param].
∀[bt:varname() List × hered-term(opr;t.P[t])].
(hered-term-accum(p,vs,v.varcase[p;vs;v]; prm,vs,f,L.m[prm;vs;f;L]; p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt]; p; bt)
∈ C[p;bt])
BY
{ (Intros
THEN ((RepeatFor 3 ((D 0 THENL [Auto; Id]))
THEN (Assert varterm(v) ∈ hered-term(opr;t.P[t]) BY
(DVar `v' THEN MemTypeCD))
THEN EAuto 1)
ORELSE (Unhide
THEN (Enough to prove ∀n:ℕ. ∀p:Param. ∀bt:varname() List × hered-term(opr;t.P[t]).
((term-size(snd(bt)) ≤ n)
⇒ (hered-term-accum(p,vs,v.varcase[p;vs;v];
prm,vs,f,L.m[prm;vs;f;L];
p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt];
p;
bt) ∈ C[p;bt]))
Because (InstHyp [⌜term-size(snd(bt))⌝;⌜p⌝;⌜bt⌝] (-1)⋅ THEN Auto))
THEN RepeatFor 2 (Thin (-1))
THEN CompleteInductionOnNat
THEN Auto
THEN RepeatFor 2 (D -2)
THEN Reduce -1
THEN (SubsumeHyp ⌜coterm-fun(opr;term(opr))⌝ (-3)⋅
THENA ((InstLemma `term-ext` [⌜opr⌝]⋅ THENA Auto) THEN D -1 THEN Auto)
)
THEN RepeatFor 2 (D -3)
THEN Unfold `hered-term-accum` 0
THEN Reduce 0
THEN Try ((All (Fold `varterm`) THEN RWO "hereditarily-varterm" (-2) THEN Auto)))
)
) }
1
1. opr : Type
2. P : term(opr) ⟶ ℙ
3. Param : Type
4. C : Param ⟶ (varname() List × hered-term(opr;t.P[t])) ⟶ Type
5. nextp : Param ⟶ (varname() List) ⟶ opr ⟶ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])
6. m : a:Param
⟶ vs:(varname() List)
⟶ f:opr
⟶ L:{L:(a:Param × bt:varname() List × hered-term(opr;t.P[t]) × C[a;bt]) List|
vdf-eq(Param;nextp a vs f;L) ∧ hereditarily(opr;s.P[s];mkterm(f;map(λx.(fst(snd(x)));L)))}
⟶ C[a;<vs, mkterm(f;map(λx.(fst(snd(x)));L))>]
7. varcase : a:Param
⟶ vs:(varname() List)
⟶ v:{v:varname()| (¬(v = nullvar() ∈ varname())) ∧ P[varterm(v)]}
⟶ C[a;<vs, varterm(v)>]
8. n : ℕ
9. ∀n:ℕn. ∀p:Param. ∀bt:varname() List × hered-term(opr;t.P[t]).
((term-size(snd(bt)) ≤ n)
⇒ (hered-term-accum(p,vs,v.varcase[p;vs;v];
prm,vs,f,L.m[prm;vs;f;L];
p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt];
p;
bt) ∈ C[p;bt]))
10. p : Param
11. b1 : varname() List
12. y1 : opr
13. y2 : (varname() List × term(opr)) List
14. hereditarily(opr;s.P[s];inr <y1, y2> )
15. term-size(inr <y1, y2> ) ≤ n
⊢ let L = bound-terms-accum(sofar,bt.nextp[p;b1;y1;sofar;bt];p',bt.hered-term-accum(p,vs,v.varcase[p;vs;v];
prm,vs,f,L.m[prm;vs;f;L];
p0,ws,op,sofar,bt.nextp[p0;ws;op;
sofar;bt];
p';
bt);y2) in
m[p;b1;y1;L] ∈ C[p;<b1, inr <y1, y2> >]
Latex:
Latex:
No Annotations
\mforall{}[opr:Type]. \mforall{}[P:term(opr) {}\mrightarrow{} \mBbbP{}]. \mforall{}[Param:Type]. \mforall{}[C:Param
{}\mrightarrow{} (varname() List \mtimes{} hered-term(opr;t.P[t]))
{}\mrightarrow{} Type].
\mforall{}[nextp:Param
{}\mrightarrow{} (varname() List)
{}\mrightarrow{} opr
{}\mrightarrow{} very-dep-fun(Param;varname() List \mtimes{} hered-term(opr;t.P[t]);a,bt.C[a;bt])].
\mforall{}[m:a:Param
{}\mrightarrow{} vs:(varname() List)
{}\mrightarrow{} f:opr
{}\mrightarrow{} L:\{L:(a:Param \mtimes{} bt:varname() List \mtimes{} hered-term(opr;t.P[t]) \mtimes{} C[a;bt]) List|
vdf-eq(Param;nextp a vs f;L)
\mwedge{} hereditarily(opr;s.P[s];mkterm(f;map(\mlambda{}x.(fst(snd(x)));L)))\}
{}\mrightarrow{} C[a;<vs, mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))>]]. \mforall{}[varcase:a:Param
{}\mrightarrow{} vs:(varname() List)
{}\mrightarrow{} v:\{v:varname()|
(\mneg{}(v = nullvar()))
\mwedge{} P[varterm(v)]\}
{}\mrightarrow{} C[a;<vs, varterm(v)>]]. \mforall{}[p:Param].
\mforall{}[bt:varname() List \mtimes{} hered-term(opr;t.P[t])].
(hered-term-accum(p,vs,v.varcase[p;vs;v];
prm,vs,f,L.m[prm;vs;f;L];
p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt];
p;
bt) \mmember{} C[p;bt])
By
Latex:
(Intros
THEN ((RepeatFor 3 ((D 0 THENL [Auto; Id]))
THEN (Assert varterm(v) \mmember{} hered-term(opr;t.P[t]) BY
(DVar `v' THEN MemTypeCD))
THEN EAuto 1)
ORELSE (Unhide
THEN (Enough to prove \mforall{}n:\mBbbN{}. \mforall{}p:Param. \mforall{}bt:varname() List \mtimes{} hered-term(opr;t.P[t]).
((term-size(snd(bt)) \mleq{} n)
{}\mRightarrow{} (hered-term-accum(p,vs,v.varcase[p;vs;v];
prm,vs,f,L.m[prm;vs;f;L];
p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;
bt];
p;
bt) \mmember{} C[p;bt]))
Because (InstHyp [\mkleeneopen{}term-size(snd(bt))\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}bt\mkleeneclose{}] (-1)\mcdot{} THEN Auto))
THEN RepeatFor 2 (Thin (-1))
THEN CompleteInductionOnNat
THEN Auto
THEN RepeatFor 2 (D -2)
THEN Reduce -1
THEN (SubsumeHyp \mkleeneopen{}coterm-fun(opr;term(opr))\mkleeneclose{} (-3)\mcdot{}
THENA ((InstLemma `term-ext` [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{} THENA Auto) THEN D -1 THEN Auto)
)
THEN RepeatFor 2 (D -3)
THEN Unfold `hered-term-accum` 0
THEN Reduce 0
THEN Try ((All (Fold `varterm`) THEN RWO "hereditarily-varterm" (-2) THEN Auto)))
)
)
Home
Index