Proof of Nuprl Lemma : term-accum_wf

Step * 1 of Lemma term-accum_wf_wfterm

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.

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
BY
{ (GenConcl ⌜(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi )
             = QQ
             ∈ (P
               ⟶ opr
               ⟶ (varname() List)
               ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List)
               ⟶ P)⌝⋅
   THENA ((MemCD THENL [Id; Auto])
          THEN (MemCD THENL [(D -3 With ⌜f⌝  THENA Auto); Auto])
          THEN (MemCD THENL [(D -2 With ⌜vs⌝  THENA Auto); Auto])
          THEN (MemCD THENL [(D -2 With ⌜L⌝  THENA Auto); Auto])
          THEN (SplitOnConclITE THENA Auto)
          THEN (Trivial

          ORELSE (ThinTrivial THEN (MemCD THENL [Auto; (MemTypeCD THEN Auto THEN UseListSubtype 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].

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. p1 : P
14. f : opr
15. vs : varname() List
16. L : (t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List
17. ↑isl(ok f vs L)
18. ||L|| < ||arity f||
19. ||vs|| = (fst(arity f[||L||])) ∈ ℤ
20. ∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ)
21. ∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))
22. L = L ∈ ({x:t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)| (x ∈ L)}  List)
23. t1 : term(opr)
24. x1 : p:P × R p t1 supposing ↑wf-term(arity;sort;t1)
25. (<t1, x1> ∈ L)
⊢ t1 ∈ wfterm(opr;sort;arity)

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

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. p1 : P
14. f : opr
15. vs : varname() List
16. L : (t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List
17. ↑isl(ok f vs L)
18. ||L|| < ||arity f||
19. ||vs|| = (fst(arity f[||L||])) ∈ ℤ
20. ∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ)
21. ∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))
22. L = L ∈ ({x:t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)| (x ∈ L)}  List)
23. t1 : term(opr)
24. p2 : P
25. x2 : R p2 t1 supposing ↑wf-term(arity;sort;t1)
26. (<t1, p2, x2> ∈ L)
⊢ x2 ∈ R p2 t1

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

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. p1 : P
14. f : opr
15. vs : varname() List
16. L : (t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List
17. ↑isl(ok f vs L)
18. ||L|| < ||arity f||
19. ||vs|| = (fst(arity f[||L||])) ∈ ℤ
20. ∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ)
21. ∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))
22. L = L ∈ ({x:t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)| (x ∈ L)}  List)
23. t1 : term(opr)
24. p2 : P
25. x2 : R p2 t1 supposing ↑wf-term(arity;sort;t1)
26. (<t1, p2, x2> ∈ L)
27. p3 : P
⊢ t1 ∈ wfterm(opr;sort;arity)

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

12. ok : ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.

13. ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.

14. QQ : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P

15. (λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi )
= QQ

∈ (P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ 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

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. \mforall{}[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]. \mforall{}[varcase:p:P {}\mrightarrow{} v:\{v:varname()| \mneg{}(v = nullvar())\} {}\mrightarrow{} R p varterm(v) supposing True]. \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)) 7. 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 8. varcase : p:P {}\mrightarrow{} v:\{v:varname()| \mneg{}(v = nullvar())\} {}\mrightarrow{} (R p varterm(v)) 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. ok : \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]))))) 13. \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]))))) \mvdash{} 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: (GenConcl \mkleeneopen{}(\mlambda{}p,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) = QQ\mkleeneclose{}\mcdot{} THENA ((MemCD THENL [Id; Auto]) THEN (MemCD THENL [(D -3 With \mkleeneopen{}f\mkleeneclose{} THENA Auto); Auto]) THEN (MemCD THENL [(D -2 With \mkleeneopen{}vs\mkleeneclose{} THENA Auto); Auto]) THEN (MemCD THENL [(D -2 With \mkleeneopen{}L\mkleeneclose{} THENA Auto); Auto]) THEN (SplitOnConclITE THENA Auto) THEN (Trivial ORELSE (ThinTrivial THEN (MemCD THENL [Auto; (MemTypeCD THEN Auto THEN UseListSubtype THEN Auto)]) ) )) ) Home Index