Nuprl Lemma : term-accum_wf_ctt1

∀[R:?CubicalContext ⟶ CttTerm ⟶ ℙ{i'''''}]. ∀[Q:?CubicalContext
                                                  ⟶ f:CttOp
                                                  ⟶ vs:(varname() List)
                                                  ⟶ {L:(t:CttTerm × p:?CubicalContext × R[p;t]) List| 
                                                      ||L|| < ||ctt-arity(f)||
                                                      ∧ (||vs|| = (fst(ctt-arity(f)[||L||])) ∈ ℤ)
                                                      ∧ (∀i:ℕ||L||
                                                           (ctt-kind(fst(L[i])) = (snd(ctt-arity(f)[i])) ∈ ℤ))} 
                                                  ⟶ ?CubicalContext]. ∀[varcase:p:?CubicalContext
                                                                                 ⟶ v:{v:varname()| 
                                                                                       ¬(v = nullvar() ∈ varname())} 
                                                                                 ⟶ R[p;varterm(v)]].
∀[mktermcase:p:?CubicalContext
             ⟶ f:CttOp
             ⟶ bts:wf-bound-terms(CttOp;λt.ctt-kind(t);λf.ctt-arity(f);f)
             ⟶ L:{L:(t:CttTerm × p:?CubicalContext × R[p;t]) List| 
                   (||L|| = ||bts|| ∈ ℤ)
                   ∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(CttOp)))
                   ∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ ?CubicalContext))} 
             ⟶ R[p;mkwfterm(f;bts)]]. ∀[t:CttTerm]. ∀[p:?CubicalContext].
  (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])


Proof



Definitions occuring in Statement :  ctt-term: CttTerm,  ctt-arity: ctt-arity(x),  ctt-kind: ctt-kind(t),  ctt-op: CttOp,  cubical-context: ?CubicalContext,  mkwfterm: mkwfterm(f;bts),  wf-bound-terms: wf-bound-terms(opr;sort;arity;f),  term-accum: term-accum,  varterm: varterm(v),  term: term(opr),  nullvar: nullvar(),  varname: varname(),  firstn: firstn(n;as),  select: L[n],  length: ||as||,  list: T List,  int_seg: {i..j-},  less_than: a < b,  uall: ∀[x:A]. B[x],  prop: ℙ,  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  pi1: fst(t),  pi2: snd(t),  all: ∀x:A. B[x],  not: ¬A,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} ,  lambda: λx.A[x],  function: x:A ⟶ B[x],  product: x:A × B[x],  natural_number: $n,  int: ℤ,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  ctt-term: CttTerm
Lemmas referenced :  term-accum_wf_wfterm,  ctt-op_wf,  cubical-context_wf,  ctt-kind_wf,  term_wf,  ctt-arity_wf
Rules used in proof :  cut,  instantiate,  introduction,  extract_by_obid,  sqequalHypSubstitution,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isectElimination,  thin,  cumulativity,  hypothesis,  lambdaEquality_alt,  hypothesisEquality,  universeIsType,  sqequalRule
Latex:
\mforall{}[R:?CubicalContext  {}\mrightarrow{}  CttTerm  {}\mrightarrow{}  \mBbbP{}\{i'''''\}].  \mforall{}[Q:?CubicalContext
                                                                                                    {}\mrightarrow{}  f:CttOp
                                                                                                    {}\mrightarrow{}  vs:(varname()  List)
                                                                                                    {}\mrightarrow{}  \{L:(t:CttTerm
                                                                                                            \mtimes{}  p:?CubicalContext
                                                                                                            \mtimes{}  R[p;t])  List| 
                                                                                                            ||L||  <  ||ctt-arity(f)||
                                                                                                            \mwedge{}  (||vs||  =  (fst(ctt-arity(f)[||L||])))
                                                                                                            \mwedge{}  (\mforall{}i:\mBbbN{}||L||
                                                                                                                      (ctt-kind(fst(L[i]))
                                                                                                                      =  (snd(ctt-arity(f)[i]))))\} 
                                                                                                    {}\mrightarrow{}  ?CubicalContext].
\mforall{}[varcase:p:?CubicalContext  {}\mrightarrow{}  v:\{v:varname()|  \mneg{}(v  =  nullvar())\}    {}\mrightarrow{}  R[p;varterm(v)]].
\mforall{}[mktermcase:p:?CubicalContext
                          {}\mrightarrow{}  f:CttOp
                          {}\mrightarrow{}  bts:wf-bound-terms(CttOp;\mlambda{}t.ctt-kind(t);\mlambda{}f.ctt-arity(f);f)
                          {}\mrightarrow{}  L:\{L:(t:CttTerm  \mtimes{}  p:?CubicalContext  \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:CttTerm].  \mforall{}[p:?CubicalContext].
    (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])


Date html generated: 2020_05_21-AM-10_32_21
Last ObjectModification: 2020_03_18-PM-02_45_46

Theory : cubical!type!theory


Home Index