Proof of Nuprl Lemma : term-accum_wf_wfterm

Step * of Lemma term-accum_wf_wfterm_0

No Annotations

∀[opr,P:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[R:P ⟶ wfterm(opr;sort;arity) ⟶ ℙ].

∀[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)]].
∀[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 RepeatFor 2 (ParallelLast')
   THEN Intros
   THEN Try ((Unhide
              THEN (SubsumeC ⌜R p t supposing ↑wf-term(arity;sort;t)⌝⋅
                    THENL [(InstHyp [⌜mktermcase⌝;⌜t⌝;⌜p⌝] (-4)⋅
                            THEN Try (Trivial)
                            THEN Try ((DVar `t' THEN Declaration)))
                          ; (DVar `t' THEN Unhide THEN Auto)]
                   )
              ))

   THEN ((RepeatFor 4 ((FunExt THENL [Id; Auto])) THEN ((Unfold `uimplies` 0 THEN MemTypeCD) THENL [Id; Auto]))

   ORELSE (Auto
           THEN DoSubsume
           THEN ((SubtypeReasoning1 THEN Auto) ORELSE Auto)
           THEN (D 0 THENA Auto)
           THEN D -1
           THEN D -2
           THEN D -1
           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

7. varcase : p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ (R p varterm(v))
8. ∀[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))
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. p1 : P
13. f : opr
14. bts : bound-term(opr) List
15. 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 p1 f (fst(bts[i])) firstn(i;L)) ∈ P))}
16. ↑wf-term(arity;sort;mkterm(f;bts))
⊢ mktermcase p1 f bts L ∈ R p1 mkterm(f;bts)

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{} 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)]]. \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 RepeatFor 2 (ParallelLast') THEN Intros THEN Try ((Unhide THEN (SubsumeC \mkleeneopen{}R p t supposing \muparrow{}wf-term(arity;sort;t)\mkleeneclose{}\mcdot{} THENL [(InstHyp [\mkleeneopen{}mktermcase\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}] (-4)\mcdot{} THEN Try (Trivial) THEN Try ((DVar `t' THEN Declaration))) ; (DVar `t' THEN Unhide THEN Auto)] ) )) THEN ((RepeatFor 4 ((FunExt THENL [Id; Auto])) THEN ((Unfold `uimplies` 0 THEN MemTypeCD) THENL [Id; Auto]) ) ORELSE (Auto THEN DoSubsume THEN ((SubtypeReasoning1 THEN Auto) ORELSE Auto) THEN (D 0 THENA Auto) THEN D -1 THEN D -2 THEN D -1 THEN Auto) )) Home Index