Nuprl Lemma : l-ordered-no_repeats

`∀[T:Type]. ∀[as:T List]. ∀[R:T ⟶ T ⟶ ℙ].`
`  (no_repeats(T;as)) supposing (l-ordered(T;x,y.R[x;y];as) and (∀x:T. (¬R[x;x])))`

Proof

Definitions occuring in Statement :  l-ordered: `l-ordered(T;x,y.R[x; y];L)` no_repeats: `no_repeats(T;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` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` uiff: `uiff(P;Q)` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False` all: `∀x:A. B[x]` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` guard: `{T}` l-ordered: `l-ordered(T;x,y.R[x; y];L)`
Lemmas referenced :  no_repeats_iff equal_wf l_before_wf no_repeats_witness l-ordered_wf all_wf not_wf list_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination independent_isectElimination lambdaFormation hypothesis dependent_functionElimination cumulativity independent_functionElimination voidElimination sqequalRule lambdaEquality because_Cache isect_memberEquality equalityTransitivity equalitySymmetry applyEquality functionExtensionality functionEquality universeEquality hyp_replacement dependent_set_memberEquality independent_pairFormation applyLambdaEquality setElimination rename

Latex:
\mforall{}[T:Type].  \mforall{}[as:T  List].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(no\_repeats(T;as))  supposing  (l-ordered(T;x,y.R[x;y];as)  and  (\mforall{}x:T.  (\mneg{}R[x;x])))

Date html generated: 2018_05_21-PM-07_39_36
Last ObjectModification: 2017_07_26-PM-05_13_53

Theory : general

Home Index