Nuprl Lemma : term-accum-induction

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


Proof



Definitions occuring in Statement :  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: ℙ,  guard: {T},  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,  implies: P ⇒ Q,  and: P ∧ Q,  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],  all: ∀x:A. B[x],  implies: P ⇒ Q,  guard: {T},  so_lambda: λ2x.t[x],  member: t ∈ T,  prop: ℙ,  subtype_rel: A ⊆r B,  nat: ℕ,  so_apply: x[s1;s2],  so_apply: x[s],  sq_stable: SqStable(P),  squash: ↓T,  uimplies: b supposing a,  coterm-fun: coterm-fun(opr;T),  varterm: varterm(v),  mkterm: mkterm(opr;bts),  bound-term: bound-term(opr),  int_seg: {i..j-},  ge: i ≥ j ,  lelt: i ≤ j < k,  and: P ∧ Q,  decidable: Dec(P),  or: P ∨ Q,  false: False,  le: A ≤ B,  uiff: uiff(P;Q),  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  pi2: snd(t),  pi1: fst(t),  so_apply: x[s1;s2;s3;s4],  assert: ↑b,  bnot: ¬bb,  bfalse: ff,  true: True,  ifthenelse: if b then t else f fi ,  btrue: tt,  unit: Unit,  bool: 𝔹,  let: let,  nat_plus: ℕ+,  cand: A c∧ B,  select: L[n],  l_member: (x ∈ l),  so_apply: x[s1;s2;s3],  so_lambda: so_lambda3,  append: as @ bs,  rev_implies: P ⇐ Q,  iff: P ⇐⇒ Q,  less_than: a < b,  sq_type: SQType(T),  it: ⋅,  nil: [],  colength: colength(L),  less_than': less_than'(a;b),  cons: [a / b],  so_lambda: λ2x y.t[x; y]
Lemmas referenced :  uniform-comp-nat-induction,  term_wf,  le_wf,  term-size_wf,  istype-nat,  term-ext,  sq_stable__le,  istype-le,  subtype_rel_transitivity,  coterm-fun_wf,  subtype_rel_weakening,  ext-eq_inversion,  term_size_var_lemma,  term_size_mkterm_lemma,  term-size-positive,  subtract_wf,  nat_properties,  decidable__le,  add-is-int-iff,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformle_wf,  itermConstant_wf,  itermSubtract_wf,  itermVar_wf,  itermAdd_wf,  istype-int,  int_formula_prop_and_lemma,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_subtract_lemma,  int_term_value_var_lemma,  int_term_value_add_lemma,  int_formula_prop_wf,  false_wf,  decidable__lt,  intformless_wf,  int_formula_prop_less_lemma,  istype-less_than,  summand-le-lsum,  list_wf,  varname_wf,  pi2_wf,  l_member_wf,  lsum_wf,  int_seg_wf,  bound-term_wf,  length_wf_nat,  set_subtype_base,  int_subtype_base,  length_wf,  select_wf,  int_seg_properties,  intformeq_wf,  int_formula_prop_eq_lemma,  pi1_wf,  firstn_wf,  mkterm_wf,  nullvar_wf,  istype-void,  varterm_wf,  istype-universe,  firstn_append,  less_than_wf,  assert_wf,  iff_weakening_uiff,  assert-bnot,  bool_subtype_base,  bool_wf,  bool_cases_sqequal,  eqff_to_assert,  iff_weakening_equal,  equal_wf,  assert_of_lt_int,  eqtt_to_assert,  lt_int_wf,  istype-false,  int_seg_subtype_nat,  top_wf,  subtype_rel_list,  length_nil,  istype-base,  stuck-spread,  length_of_nil_lemma,  nat_plus_properties,  add_nat_plus,  length_of_cons_lemma,  let_wf,  append_wf,  list_ind_nil_lemma,  list_ind_cons_lemma,  append_assoc,  cons_member,  subtype_rel_sets_simple,  cons_wf,  subtype_rel_dep_function,  list_accum_cons_lemma,  decidable__equal_int,  spread_cons_lemma,  length-append,  subtype_base_sq,  subtract-1-ge-0,  colength_wf_list,  colength-cons-not-zero,  product_subtype_list,  subtype_rel_self,  nil_wf,  append_back_nil,  list_accum_nil_lemma,  list-cases,  ge_wf,  select-append,  firstn_length,  lelt_wf,  non_neg_length,  assert_of_le_int,  le_int_wf,  firstn-append
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  lambdaFormation_alt,  cut,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  sqequalRule,  lambdaEquality_alt,  functionEquality,  setEquality,  hypothesisEquality,  hypothesis,  applyEquality,  because_Cache,  setElimination,  rename,  independent_functionElimination,  imageMemberEquality,  baseClosed,  imageElimination,  setIsType,  universeIsType,  independent_isectElimination,  inhabitedIsType,  unionElimination,  dependent_functionElimination,  Error :memTop,  natural_numberEquality,  productElimination,  dependent_set_memberEquality_alt,  independent_pairFormation,  pointwiseFunctionality,  equalityTransitivity,  equalitySymmetry,  promote_hyp,  baseApply,  closedConclusion,  approximateComputation,  dependent_pairFormation_alt,  int_eqEquality,  voidElimination,  productIsType,  productEquality,  independent_pairEquality,  addEquality,  equalityIstype,  isectIsType,  functionIsType,  intEquality,  sqequalBase,  universeEquality,  instantiate,  equalityElimination,  cumulativity,  voidEquality,  functionExtensionality,  dependent_pairEquality_alt,  inrFormation_alt,  applyLambdaEquality,  hypothesis_subsumption,  functionIsTypeImplies,  axiomEquality,  intWeakElimination
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{}p:P.  \mforall{}v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  .    R[p;varterm(v)])
        {}\mRightarrow{}  (\mforall{}p:P.  \mforall{}f:opr.  \mforall{}bts:bound-term(opr)  List.  \mforall{}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)]))\}  .
                    R[p;mkterm(f;bts)])
        {}\mRightarrow{}  \{\mforall{}t:term(opr).  \mforall{}p:P.    R[p;t]\})


Date html generated: 2020_05_19-PM-09_55_02
Last ObjectModification: 2020_03_12-AM-10_44_27

Theory : terms


Home Index