### Nuprl Lemma : no-repeats-pairwise

`∀[T:Type]`
`  ∀L:T List`
`    ∀[P:{x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ']`
`      (∀x,y:{x:T| (x ∈ L)} .  P[x;y] supposing ¬(x = y ∈ T)) `` (∀x,y∈L.  P[x;y]) supposing no_repeats(T;L)`

Proof

Definitions occuring in Statement :  pairwise: `(∀x,y∈L.  P[x; y])` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` implies: `P `` Q` pairwise: `(∀x,y∈L.  P[x; y])` no_repeats: `no_repeats(T;l)` prop: `ℙ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_apply: `x[s]` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` less_than: `a < b` squash: `↓T` le: `A ≤ B` less_than': `less_than'(a;b)` nat: `ℕ` ge: `i ≥ j `
Lemmas referenced :  int_seg_wf nat_wf int_formula_prop_eq_lemma intformeq_wf le_wf nat_properties length_wf false_wf int_seg_subtype_nat int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le int_seg_properties list-subtype select_wf list_wf no_repeats_wf equal_wf not_wf isect_wf l_member_wf all_wf no_repeats_witness
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis rename instantiate setEquality cumulativity applyEquality lambdaEquality universeEquality sqequalRule setElimination because_Cache dependent_set_memberEquality dependent_functionElimination functionEquality equalityTransitivity equalitySymmetry independent_isectElimination productElimination unionElimination natural_numberEquality dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination

Latex:
\mforall{}[T:Type]
\mforall{}L:T  List
\mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}']
(\mforall{}x,y:\{x:T|  (x  \mmember{}  L)\}  .    P[x;y]  supposing  \mneg{}(x  =  y))  {}\mRightarrow{}  (\mforall{}x,y\mmember{}L.    P[x;y])
supposing  no\_repeats(T;L)

Date html generated: 2016_05_14-PM-03_07_47
Last ObjectModification: 2016_01_15-AM-07_18_33

Theory : list_1

Home Index