### Nuprl Lemma : pairwise-mapl-no-repeats

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

Proof

Definitions occuring in Statement :  mapl: `mapl(f;l)` 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]} ` apply: `f a` 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]` member: `t ∈ T` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` prop: `ℙ` uimplies: `b supposing a` implies: `P `` Q` so_apply: `x[s1;s2]` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` mapl: `mapl(f;l)` top: `Top` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` true: `True` or: `P ∨ Q` guard: `{T}` cand: `A c∧ B` uiff: `uiff(P;Q)` not: `¬A` false: `False` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` less_than: `a < b` squash: `↓T`
Lemmas referenced :  list_induction all_wf l_member_wf uall_wf isect_wf no_repeats_wf not_wf equal_wf pairwise_wf2 mapl_wf list_wf no_repeats_witness nil_wf map_nil_lemma pairwise-nil cons_wf map_cons_lemma pairwise-cons cons_member subtype_rel_dep_function subtype_rel_sets set_wf no_repeats_cons member-mapl select_wf int_seg_properties length_wf decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma select_member int_seg_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality sqequalRule lambdaEquality functionEquality setEquality because_Cache hypothesis applyEquality universeEquality setElimination rename isectEquality functionExtensionality dependent_set_memberEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality productElimination natural_numberEquality inlFormation independent_isectElimination inrFormation independent_pairFormation equalityTransitivity equalitySymmetry unionElimination dependent_pairFormation int_eqEquality intEquality computeAll imageElimination hyp_replacement applyLambdaEquality

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

Date html generated: 2017_04_17-AM-08_41_39
Last ObjectModification: 2017_02_27-PM-05_00_20

Theory : list_1

Home Index