Nuprl Lemma : no_repeats-length-equal-by-relation

∀[A,B:Type]. ∀[as:A List]. ∀[bs:B List].
  (||as|| = ||bs|| ∈ ℤ) supposing 
     ((∃R:A ⟶ B ⟶ ℙ
        ((∀a1,a2:A. ∀b:B.  ((a1 ∈ as) ⇒ (a2 ∈ as) ⇒ (b ∈ bs) ⇒ (R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A)))
        ∧ (∀b1,b2:B. ∀a:A.  ((b1 ∈ bs) ⇒ (b2 ∈ bs) ⇒ (a ∈ as) ⇒ (R a b1) ⇒ (R a b2) ⇒ (b1 = b2 ∈ B)))
        ∧ (∀a∈as.(∃b∈bs. R a b))
        ∧ (∀b∈bs.(∃a∈as. R a b)))) and 
     no_repeats(A;as) and 
     no_repeats(B;bs))


Proof



Definitions occuring in Statement :  l_exists: (∃x∈L. P[x]),  l_all: (∀x∈L.P[x]),  no_repeats: no_repeats(T;l),  l_member: (x ∈ l),  length: ||as||,  list: T List,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  prop: ℙ,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  apply: f a,  function: x:A ⟶ B[x],  int: ℤ,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  exists: ∃x:A. B[x],  and: P ∧ Q,  all: ∀x:A. B[x],  implies: P ⇒ Q,  subtype_rel: A ⊆r B,  decidable: Dec(P),  or: P ∨ Q,  le: A ≤ B,  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  false: False,  top: Top,  prop: ℙ,  so_lambda: λ2x.t[x],  so_apply: x[s],  guard: {T},  cand: A c∧ B,  l_all: (∀x∈L.P[x]),  l_exists: (∃x∈L. P[x]),  int_seg: {i..j-},  lelt: i ≤ j < k,  less_than: a < b,  squash: ↓T
Lemmas referenced :  no_repeats-length-le-by-relation,  decidable__equal_int,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformeq_wf,  itermVar_wf,  intformle_wf,  istype-int,  int_formula_prop_and_lemma,  istype-void,  int_formula_prop_not_lemma,  int_formula_prop_eq_lemma,  int_term_value_var_lemma,  int_formula_prop_le_lemma,  int_formula_prop_wf,  subtype_rel_self,  l_all_wf,  l_exists_wf,  l_member_wf,  no_repeats_wf,  list_wf,  istype-universe,  select_member,  select_wf,  int_seg_properties,  decidable__le,  itermConstant_wf,  int_term_value_constant_lemma,  decidable__lt,  length_wf,  intformless_wf,  int_formula_prop_less_lemma,  int_seg_wf
Rules used in proof :  cut,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  introduction,  sqequalHypSubstitution,  productElimination,  thin,  extract_by_obid,  isectElimination,  hypothesisEquality,  independent_isectElimination,  hypothesis,  because_Cache,  lambdaEquality_alt,  applyEquality,  universeIsType,  lambdaFormation_alt,  sqequalRule,  inhabitedIsType,  dependent_functionElimination,  unionElimination,  natural_numberEquality,  approximateComputation,  independent_functionElimination,  dependent_pairFormation_alt,  int_eqEquality,  isect_memberEquality_alt,  voidElimination,  independent_pairFormation,  productIsType,  functionIsType,  universeEquality,  instantiate,  equalityIstype,  setElimination,  rename,  setIsType,  axiomEquality,  isectIsTypeImplies,  productEquality,  imageElimination
Latex:
\mforall{}[A,B:Type].  \mforall{}[as:A  List].  \mforall{}[bs:B  List].
    (||as||  =  ||bs||)  supposing 
          ((\mexists{}R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
                ((\mforall{}a1,a2:A.  \mforall{}b:B.
                        ((a1  \mmember{}  as)  {}\mRightarrow{}  (a2  \mmember{}  as)  {}\mRightarrow{}  (b  \mmember{}  bs)  {}\mRightarrow{}  (R  a1  b)  {}\mRightarrow{}  (R  a2  b)  {}\mRightarrow{}  (a1  =  a2)))
                \mwedge{}  (\mforall{}b1,b2:B.  \mforall{}a:A.
                          ((b1  \mmember{}  bs)  {}\mRightarrow{}  (b2  \mmember{}  bs)  {}\mRightarrow{}  (a  \mmember{}  as)  {}\mRightarrow{}  (R  a  b1)  {}\mRightarrow{}  (R  a  b2)  {}\mRightarrow{}  (b1  =  b2)))
                \mwedge{}  (\mforall{}a\mmember{}as.(\mexists{}b\mmember{}bs.  R  a  b))
                \mwedge{}  (\mforall{}b\mmember{}bs.(\mexists{}a\mmember{}as.  R  a  b))))  and 
          no\_repeats(A;as)  and 
          no\_repeats(B;bs))


Date html generated: 2020_05_19-PM-09_42_58
Last ObjectModification: 2019_10_23-PM-04_21_45

Theory : list_1


Home Index