Nuprl Lemma : alpha-aux-mkterm

∀[opr:Type]
  ∀a,b:opr. ∀as,bs:bound-term(opr) List. ∀vs,ws:varname() List.
    (alpha-aux(opr;vs;ws;mkterm(a;as);mkterm(b;bs))
    ⇐⇒ (a = b ∈ opr)
        ∧ (||as|| = ||bs|| ∈ ℤ)
        ∧ (∀i:ℕ||as||
             (alpha-aux(opr;rev(fst(as[i])) + vs;rev(fst(bs[i])) + ws;snd(as[i]);snd(bs[i]))
             ∧ (||fst(as[i])|| = ||fst(bs[i])|| ∈ ℤ))))


Proof



Definitions occuring in Statement :  alpha-aux: alpha-aux(opr;vs;ws;a;b),  bound-term: bound-term(opr),  mkterm: mkterm(opr;bts),  varname: varname(),  select: L[n],  length: ||as||,  rev-append: rev(as) + bs,  list: T List,  int_seg: {i..j-},  uall: ∀[x:A]. B[x],  pi1: fst(t),  pi2: snd(t),  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  and: P ∧ Q,  natural_number: $n,  int: ℤ,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  member: t ∈ T,  so_lambda: λ2x.t[x],  bound-term: bound-term(opr),  prop: ℙ,  and: P ∧ Q,  implies: P ⇒ Q,  pi2: snd(t),  pi1: fst(t),  subtype_rel: A ⊆r B,  nat: ℕ,  int_seg: {i..j-},  lelt: i ≤ j < k,  le: A ≤ B,  so_apply: x[s],  uimplies: b supposing a,  select: L[n],  nil: [],  it: ⋅,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  false: False,  alpha-aux: alpha-aux(opr;vs;ws;a;b),  mkterm: mkterm(opr;bts),  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  cons: [a / b],  ge: i ≥ j ,  decidable: Dec(P),  or: P ∨ Q,  sq_type: SQType(T),  guard: {T},  less_than': less_than'(a;b),  nat_plus: ℕ+,  uiff: uiff(P;Q),  less_than: a < b,  squash: ↓T,  label: ...$L... t,  true: True,  subtract: n - m
Lemmas referenced :  list_induction,  bound-term_wf,  all_wf,  list_wf,  varname_wf,  iff_wf,  alpha-aux_wf,  mkterm_wf,  equal_wf,  equal-wf-base,  int_seg_wf,  rev-append_wf,  length_wf_nat,  set_subtype_base,  le_wf,  int_subtype_base,  length_wf,  length_of_nil_lemma,  stuck-spread,  istype-base,  nil_wf,  term_wf,  int_seg_properties,  full-omega-unsat,  intformand_wf,  intformless_wf,  itermVar_wf,  itermConstant_wf,  intformle_wf,  istype-int,  int_formula_prop_and_lemma,  int_formula_prop_less_lemma,  int_term_value_var_lemma,  int_term_value_constant_lemma,  int_formula_prop_le_lemma,  int_formula_prop_wf,  length_of_cons_lemma,  non_neg_length,  decidable__le,  intformnot_wf,  int_formula_prop_not_lemma,  istype-void,  intformeq_wf,  itermAdd_wf,  int_formula_prop_eq_lemma,  int_term_value_add_lemma,  cons_wf,  spread_cons_lemma,  decidable__equal_int,  subtype_base_sq,  select_wf,  decidable__lt,  istype-false,  add_nat_plus,  istype-less_than,  nat_plus_properties,  add-is-int-iff,  false_wf,  istype-le,  subtype_rel_self,  istype-universe,  select-cons-tl,  subtract_wf,  itermSubtract_wf,  int_term_value_subtract_lemma,  select_cons_tl_sq2,  int_seg_subtype_nat,  add-associates,  add-swap,  add-commutes,  zero-add,  squash_wf,  true_wf,  iff_weakening_equal,  add-subtract-cancel
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  lambdaFormation_alt,  cut,  thin,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  hypothesis,  sqequalRule,  lambdaEquality_alt,  because_Cache,  productEquality,  closedConclusion,  natural_numberEquality,  equalityTransitivity,  equalitySymmetry,  inhabitedIsType,  productElimination,  equalityIstype,  dependent_functionElimination,  independent_functionElimination,  applyEquality,  setElimination,  rename,  independent_isectElimination,  universeIsType,  baseClosed,  Error :memTop,  approximateComputation,  dependent_pairFormation_alt,  int_eqEquality,  independent_pairFormation,  voidElimination,  productIsType,  sqequalBase,  functionIsType,  unionElimination,  addEquality,  intEquality,  independent_pairEquality,  instantiate,  cumulativity,  dependent_set_memberEquality_alt,  applyLambdaEquality,  pointwiseFunctionality,  promote_hyp,  baseApply,  imageElimination,  universeEquality,  imageMemberEquality
Latex:
\mforall{}[opr:Type]
    \mforall{}a,b:opr.  \mforall{}as,bs:bound-term(opr)  List.  \mforall{}vs,ws:varname()  List.
        (alpha-aux(opr;vs;ws;mkterm(a;as);mkterm(b;bs))
        \mLeftarrow{}{}\mRightarrow{}  (a  =  b)
                \mwedge{}  (||as||  =  ||bs||)
                \mwedge{}  (\mforall{}i:\mBbbN{}||as||
                          (alpha-aux(opr;rev(fst(as[i]))  +  vs;rev(fst(bs[i]))  +  ws;snd(as[i]);snd(bs[i]))
                          \mwedge{}  (||fst(as[i])||  =  ||fst(bs[i])||))))


Date html generated: 2020_05_19-PM-09_55_28
Last ObjectModification: 2020_03_09-PM-04_08_55

Theory : terms


Home Index