Proof of Nuprl Lemma : hered-term-accum

Step * 1 1 1 of Lemma hered-term-accum_wf

.....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]

BY
{ ((RepeatFor 2 ((FunExt THENW Auto)) THEN Reduce 0)
   THEN (Enough to prove term-size(snd(bt)) < term-size(inr <y1, y2> )
          Because (InstHyp [⌜n - 1⌝] 9⋅ THEN Auto))
   THEN Fold `mkterm` 0
   THEN Reduce 0
   THEN D -1) }

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])

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. a : Param
19. bt : varname() List × hered-term(opr;t.P[t])
20. (bt ∈ y2)
⊢ term-size(snd(bt)) < 1 + Σ(term-size(snd(bt)) | bt ∈ y2)

Latex:

Latex:
.....wf..... 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 \mvdash{} \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) \mmember{} a:Param {}\mrightarrow{} bt:\{bt:varname() List \mtimes{} hered-term(opr;t.P[t])| (bt \mmember{} y2)\} {}\mrightarrow{} C[a;bt] By Latex: ((RepeatFor 2 ((FunExt THENW Auto)) THEN Reduce 0) THEN (Enough to prove term-size(snd(bt)) < term-size(inr <y1, y2> ) Because (InstHyp [\mkleeneopen{}n - 1\mkleeneclose{}] 9\mcdot{} THEN Auto)) THEN Fold `mkterm` 0 THEN Reduce 0 THEN D -1) Home Index