Nuprl Lemma : term-accum_wf

∀[opr,P:Type]. ∀[R:P ⟶ term(opr) ⟶ ℙ]. ∀[Q:P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P].
∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ R[p;varterm(v)]].
∀[mktermcase:p:P
             ⟶ f:opr
             ⟶ bts:(bound-term(opr) List)
             ⟶ L:{L:(t:term(opr) × 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;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])


Proof



Definitions occuring in Statement :  term-accum: term-accum,  bound-term: bound-term(opr),  mkterm: mkterm(opr;bts),  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-},  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]} ,  function: x:A ⟶ B[x],  product: x:A × B[x],  natural_number: $n,  int: ℤ,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  so_apply: x[s1;s2],  all: ∀x:A. B[x],  so_apply: x[s1;s2;s3;s4],  and: P ∧ Q,  term-accum: term-accum,  subtype_rel: A ⊆r B,  nat: ℕ,  so_lambda: λ2x.t[x],  so_apply: x[s],  uimplies: b supposing a,  int_seg: {i..j-},  lelt: i ≤ j < k,  le: A ≤ B,  decidable: Dec(P),  or: P ∨ Q,  not: ¬A,  implies: P ⇒ Q,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  false: False,  prop: ℙ,  pi1: fst(t),  bound-term: bound-term(opr),  pi2: snd(t)
Lemmas referenced :  term-accum1_wf,  term_wf,  list_wf,  bound-term_wf,  istype-int,  length_wf_nat,  set_subtype_base,  le_wf,  int_subtype_base,  int_seg_wf,  length_wf,  select_wf,  int_seg_properties,  decidable__le,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformle_wf,  itermConstant_wf,  itermVar_wf,  int_formula_prop_and_lemma,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_var_lemma,  int_formula_prop_wf,  decidable__lt,  intformless_wf,  int_formula_prop_less_lemma,  intformeq_wf,  int_formula_prop_eq_lemma,  pi1_wf,  firstn_wf,  mkterm_wf,  varname_wf,  nullvar_wf,  istype-void,  varterm_wf,  subtype_rel_self,  istype-universe
Rules used in proof :  cut,  introduction,  extract_by_obid,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  hypothesis,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  sqequalRule,  applyEquality,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  universeIsType,  functionIsType,  setIsType,  productEquality,  because_Cache,  productIsType,  equalityIstype,  intEquality,  lambdaEquality_alt,  natural_numberEquality,  independent_isectElimination,  sqequalBase,  setElimination,  rename,  productElimination,  dependent_functionElimination,  unionElimination,  approximateComputation,  independent_functionElimination,  dependent_pairFormation_alt,  int_eqEquality,  Error :memTop,  independent_pairFormation,  voidElimination,  inhabitedIsType,  lambdaFormation_alt,  instantiate,  universeEquality
Latex:
\mforall{}[opr,P:Type].  \mforall{}[R:P  {}\mrightarrow{}  term(opr)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:P
                                                                                          {}\mrightarrow{}  opr
                                                                                          {}\mrightarrow{}  (varname()  List)
                                                                                          {}\mrightarrow{}  ((t:term(opr)  \mtimes{}  p:P  \mtimes{}  R[p;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:(bound-term(opr)  List)
                          {}\mrightarrow{}  L:\{L:(t:term(opr)  \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;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])


Date html generated: 2020_05_19-PM-09_55_14
Last ObjectModification: 2020_03_09-PM-04_08_45

Theory : terms


Home Index