Nuprl Lemma : permr_upto_weakening

T:Type. ∀R:T ⟶ T ⟶ ℙ.  (EquivRel(T;x,y.R[x;y])  (∀as,bs:T List.  ((as ≡(T) bs)  as ≡ bs upto x,y.R[x;y] )))


Proof




Definitions occuring in Statement :  permr_upto: as ≡ bs upto x,y.R[x; y]  permr: as ≡(T) bs list: List equiv_rel: EquivRel(T;x,y.E[x; y]) prop: so_apply: x[s1;s2] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] permr: as ≡(T) bs permr_upto: as ≡ bs upto x,y.R[x; y]  cand: c∧ B exists: x:A. B[x] sym_grp: Sym(n) perm: Perm(T) subtype_rel: A ⊆B uimplies: supposing a ge: i ≥  guard: {T} int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q decidable: Dec(P) or: P ∨ Q false: False nat: less_than: a < b squash: T not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top iff: ⇐⇒ Q rev_implies:  Q equiv_rel: EquivRel(T;x,y.E[x; y]) refl: Refl(T;x,y.E[x; y])
Lemmas referenced :  permr_wf list_wf equiv_rel_wf istype-universe int_seg_wf length_wf select_wf perm_f_wf non_neg_length int_seg_properties decidable__le le_wf less_than_wf length_wf_nat nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformnot_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma intformeq_wf int_formula_prop_eq_lemma subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis inhabitedIsType isectElimination sqequalRule lambdaEquality_alt applyEquality functionIsType universeEquality productElimination independent_pairFormation dependent_pairFormation_alt natural_numberEquality equalityTransitivity equalitySymmetry setElimination rename because_Cache independent_isectElimination dependent_set_memberEquality_alt productIsType unionElimination applyLambdaEquality imageElimination approximateComputation independent_functionElimination int_eqEquality isect_memberEquality_alt voidElimination instantiate

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    (EquivRel(T;x,y.R[x;y])  {}\mRightarrow{}  (\mforall{}as,bs:T  List.    ((as  \mequiv{}(T)  bs)  {}\mRightarrow{}  as  \mequiv{}  bs  upto  x,y.R[x;y]  )))



Date html generated: 2019_10_16-PM-01_01_19
Last ObjectModification: 2018_10_08-PM-00_47_55

Theory : perms_2


Home Index