Nuprl Lemma : hered-term-accum_wf

∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[Param:Type]. ∀[C:Param ⟶ (varname() List × hered-term(opr;t.P[t])) ⟶ Type].
∀[nextp:Param ⟶ (varname() List) ⟶ opr ⟶ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])].
∀[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))>]]. ∀[varcase:a:Param
                                                             ⟶ vs:(varname() List)
                                                             ⟶ v:{v:varname()| 
                                                                   (¬(v = nullvar() ∈ varname())) ∧ P[varterm(v)]} 
                                                             ⟶ C[a;<vs, varterm(v)>]]. ∀[p:Param].
∀[bt:varname() List × hered-term(opr;t.P[t])].
  (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])


Proof



Definitions occuring in Statement :  hered-term-accum: hered-term-accum,  hered-term: hered-term(opr;t.P[t]),  hereditarily: hereditarily(opr;s.P[s];t),  mkterm: mkterm(opr;bts),  varterm: varterm(v),  term: term(opr),  nullvar: nullvar(),  varname: varname(),  very-dep-fun: very-dep-fun(A;B;a,b.C[a; b]),  vdf-eq: vdf-eq(A;f;L),  map: map(f;as),  list: T List,  uall: ∀[x:A]. B[x],  prop: ℙ,  so_apply: x[s1;s2;s3;s4;s5],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2],  so_apply: x[s],  pi1: fst(t),  pi2: snd(t),  not: ¬A,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} ,  apply: f a,  lambda: λx.A[x],  function: x:A ⟶ B[x],  pair: <a, b>,  product: x:A × B[x],  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  all: ∀x:A. B[x],  nat: ℕ,  implies: P ⇒ Q,  false: False,  ge: i ≥ j ,  uimplies: b supposing a,  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  and: P ∧ Q,  prop: ℙ,  guard: {T},  int_seg: {i..j-},  lelt: i ≤ j < k,  le: A ≤ B,  decidable: Dec(P),  or: P ∨ Q,  subtype_rel: A ⊆r B,  so_lambda: λ2x.t[x],  so_apply: x[s],  sq_type: SQType(T),  hered-term: hered-term(opr;t.P[t]),  pi2: snd(t),  ext-eq: A ≡ B,  coterm-fun: coterm-fun(opr;T),  hered-term-accum: hered-term-accum,  varterm: varterm(v),  iff: P ⇐⇒ Q,  so_apply: x[s1;s2;s3],  rev_implies: P ⇐ Q,  so_apply: x[s1;s2],  so_lambda: λ2x y.t[x; y],  pi1: fst(t),  so_apply: x[s1;s2;s3;s4;s5],  so_apply: x[s1;s2;s3;s4],  mkterm: mkterm(opr;bts),  bound-term: bound-term(opr),  less_than: a < b,  squash: ↓T,  less_than': less_than'(a;b),  true: True,  l_member: (x ∈ l),  cand: A c∧ B,  sq_stable: SqStable(P),  respects-equality: respects-equality(S;T),  let: let
Lemmas referenced :  nat_properties,  full-omega-unsat,  intformand_wf,  intformle_wf,  itermConstant_wf,  itermVar_wf,  intformless_wf,  istype-int,  int_formula_prop_and_lemma,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_var_lemma,  int_formula_prop_less_lemma,  int_formula_prop_wf,  ge_wf,  istype-less_than,  int_seg_properties,  int_seg_wf,  subtract-1-ge-0,  decidable__equal_int,  subtract_wf,  subtype_base_sq,  set_subtype_base,  int_subtype_base,  intformnot_wf,  intformeq_wf,  itermSubtract_wf,  int_formula_prop_not_lemma,  int_formula_prop_eq_lemma,  int_term_value_subtract_lemma,  decidable__le,  decidable__lt,  istype-le,  subtype_rel_self,  term-ext,  hereditarily-varterm,  term_wf,  nullvar_wf,  istype-void,  varterm_wf,  term-size_wf,  pi2_wf,  list_wf,  varname_wf,  hered-term_wf,  itermAdd_wf,  int_term_value_add_lemma,  istype-nat,  hereditarily_wf,  vdf-eq_wf,  mkterm_wf,  map_wf,  trivial-equal,  very-dep-fun_wf,  istype-universe,  very-dep-fun-eta,  hereditarily-mkterm,  list-subtype,  subtype_rel_list,  l_member_wf,  bound-terms-accum_wf,  term_size_mkterm_lemma,  easy-member-int_seg,  summand-le-lsum,  sq_stable__le,  non_neg_length,  length_wf,  subtype_rel_product,  equal_functionality_wrt_subtype_rel2,  select_wf,  respects-equality-product,  respects-equality-trivial,  respects-equality-set-trivial2,  istype-base,  lsum_wf,  equal_wf,  squash_wf,  true_wf,  iff_weakening_equal
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  cut,  thin,  lambdaFormation_alt,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  hypothesis,  setElimination,  rename,  sqequalRule,  intWeakElimination,  natural_numberEquality,  independent_isectElimination,  approximateComputation,  independent_functionElimination,  dependent_pairFormation_alt,  lambdaEquality_alt,  int_eqEquality,  dependent_functionElimination,  Error :memTop,  independent_pairFormation,  universeIsType,  voidElimination,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  functionIsTypeImplies,  inhabitedIsType,  productElimination,  unionElimination,  applyEquality,  instantiate,  because_Cache,  applyLambdaEquality,  dependent_set_memberEquality_alt,  productIsType,  promote_hyp,  hypothesis_subsumption,  functionIsType,  equalityIstype,  addEquality,  independent_pairEquality,  setIsType,  productEquality,  universeEquality,  setEquality,  functionExtensionality,  closedConclusion,  imageMemberEquality,  baseClosed,  imageElimination,  sqequalBase,  hyp_replacement
Latex:
\mforall{}[opr:Type].  \mforall{}[P:term(opr)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Param:Type].  \mforall{}[C:Param
                                                                                                          {}\mrightarrow{}  (varname()  List  \mtimes{}  hered-term(opr;t.P[t]))
                                                                                                          {}\mrightarrow{}  Type].
\mforall{}[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])].
\mforall{}[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))>]].  \mforall{}[varcase:a:Param
                                                                                                                          {}\mrightarrow{}  vs:(varname()  List)
                                                                                                                          {}\mrightarrow{}  v:\{v:varname()| 
                                                                                                                                      (\mneg{}(v  =  nullvar()))
                                                                                                                                      \mwedge{}  P[varterm(v)]\} 
                                                                                                                          {}\mrightarrow{}  C[a;<vs,  varterm(v)>]].  \mforall{}[p:Param].
\mforall{}[bt:varname()  List  \mtimes{}  hered-term(opr;t.P[t])].
    (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])


Date html generated: 2020_05_19-PM-09_54_54
Last ObjectModification: 2020_03_10-PM-05_50_07

Theory : terms


Home Index