Step
*
1
1
of Lemma
hered-term-accum_wf
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
16. λsofar,bt. nextp[p;b1;y1;sofar;bt] ∈ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])
17. y2 ∈ (varname() List × hered-term(opr;t.P[t])) List
18. ∀[g:a:Param ⟶ bt:{bt:varname() List × hered-term(opr;t.P[t])| (bt ∈ y2)} ⟶ C[a;bt]]
(bound-terms-accum(L,bt.nextp[p;b1;y1;L;bt];a,bt.g[a;bt];y2) ∈ {L:(a:Param
× b:varname() List × hered-term(opr;t.P[t])
× C[a;b]) List|
vdf-eq(Param;λ2sofar bt.nextp[p;b1;y1;sofar;bt];L)
∧ (map(λx.(fst(snd(x)));L)
= y2
∈ ((varname() List
× hered-term(opr;t.P[t])) List))} )
⊢ 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> >]
BY
{ D -1 With ⌜λ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)⌝ }
1
.....wf.....
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
16. λsofar,bt. nextp[p;b1;y1;sofar;bt] ∈ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])
17. y2 ∈ (varname() List × hered-term(opr;t.P[t])) List
⊢ λ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) ∈ a:Param ⟶ bt:{bt:varname() List × hered-term(opr;t.P[t])| (bt ∈ y2)} ⟶ C[a;bt]
2
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
16. λsofar,bt. nextp[p;b1;y1;sofar;bt] ∈ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])
17. y2 ∈ (varname() List × hered-term(opr;t.P[t])) List
18. bound-terms-accum(L,bt.nextp[p;b1;y1;L;bt];a,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)[a;bt];y2)
∈ {L:(a:Param × b:varname() List × hered-term(opr;t.P[t]) × C[a;b]) List|
vdf-eq(Param;λ2sofar bt.nextp[p;b1;y1;sofar;bt];L)
∧ (map(λx.(fst(snd(x)));L) = y2 ∈ ((varname() List × hered-term(opr;t.P[t])) List))}
⊢ 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:
1. opr : Type
2. P : term(opr) {}\mrightarrow{} \mBbbP{}
3. Param : Type
4. C : Param {}\mrightarrow{} (varname() List \mtimes{} hered-term(opr;t.P[t])) {}\mrightarrow{} Type
5. 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])
6. 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))>]
7. varcase : a:Param
{}\mrightarrow{} vs:(varname() List)
{}\mrightarrow{} v:\{v:varname()| (\mneg{}(v = nullvar())) \mwedge{} P[varterm(v)]\}
{}\mrightarrow{} C[a;<vs, varterm(v)>]
8. n : \mBbbN{}
9. \mforall{}n:\mBbbN{}n. \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]))
10. p : Param
11. b1 : varname() List
12. y1 : opr
13. y2 : (varname() List \mtimes{} term(opr)) List
14. hereditarily(opr;s.P[s];inr <y1, y2> )
15. term-size(inr <y1, y2> ) \mleq{} n
16. \mlambda{}sofar,bt. nextp[p;b1;y1;sofar;bt] \mmember{} very-dep-fun(Param;varname() List
\mtimes{} hered-term(opr;t.P[t]);a,bt.C[a;bt])
17. y2 \mmember{} (varname() List \mtimes{} hered-term(opr;t.P[t])) List
18. \mforall{}[g:a:Param {}\mrightarrow{} bt:\{bt:varname() List \mtimes{} hered-term(opr;t.P[t])| (bt \mmember{} y2)\} {}\mrightarrow{} C[a;bt]]
(bound-terms-accum(L,bt.nextp[p;b1;y1;L;bt];a,bt.g[a;bt];y2)
\mmember{} \{L:(a:Param \mtimes{} b:varname() List \mtimes{} hered-term(opr;t.P[t]) \mtimes{} C[a;b]) List|
vdf-eq(Param;\mlambda{}\msubtwo{}sofar bt.nextp[p;b1;y1;sofar;bt];L) \mwedge{} (map(\mlambda{}x.(fst(snd(x)));L) = y2)\} )
\mvdash{} 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] \mmember{} C[p;<b1, inr <y1, y2> >]
By
Latex:
D -1 With \mkleeneopen{}\mlambda{}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)\mkleeneclose{}
Home
Index