### Nuprl Lemma : sublist-if-no_repeats

`∀[A:Type]`
`  ∀R:A ⟶ A ⟶ 𝔹. ∀as,bs:A List.`
`    (StAntiSym(A;x,y.↑R[x;y])`
`    `` Irrefl(A;x,y.↑R[x;y])`
`    `` Trans(A;x,y.↑R[x;y])`
`    `` no_repeats(A;as)`
`    `` l-ordered(A;x,y.↑R[x;y];as)`
`    `` l-ordered(A;x,y.↑R[x;y];bs)`
`    `` (∀a∈as.(a ∈ bs))`
`    `` as ⊆ bs)`

Proof

Definitions occuring in Statement :  l-ordered: `l-ordered(T;x,y.R[x; y];L)` sublist: `L1 ⊆ L2` l_all: `(∀x∈L.P[x])` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` list: `T List` irrefl: `Irrefl(T;x,y.E[x; y])` st_anti_sym: `StAntiSym(T;x,y.R[x; y])` trans: `Trans(T;x,y.E[x; y])` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` so_apply: `x[s]` top: `Top` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` not: `¬A` false: `False` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` or: `P ∨ Q` cand: `A c∧ B` rev_implies: `P `` Q` st_anti_sym: `StAntiSym(T;x,y.R[x; y])` guard: `{T}`
Lemmas referenced :  list_induction all_wf list_wf st_anti_sym_wf assert_wf irrefl_wf trans_wf no_repeats_wf l-ordered_wf l_all_wf2 l_member_wf sublist_wf nil-sublist true_wf no_repeats_nil_uiff l-ordered-nil-true l_all_nil_iff nil_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse l-ordered-decomp2 sublist_append cons_wf filter_wf5 list_ind_nil_lemma not_wf no_repeats_cons l-ordered-cons l_all_cons bool_wf cons_sublist_cons l-ordered-append l_all_iff append_wf member_append member_filter_2 member_filter cons_member and_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis functionEquality because_Cache applyEquality functionExtensionality setElimination rename setEquality independent_functionElimination isect_memberEquality voidElimination voidEquality addLevel allFunctionality impliesFunctionality productElimination independent_isectElimination equalityTransitivity equalitySymmetry dependent_functionElimination hyp_replacement Error :applyLambdaEquality,  productEquality universeEquality inlFormation independent_pairFormation levelHypothesis promote_hyp unionElimination allLevelFunctionality impliesLevelFunctionality dependent_set_memberEquality

Latex:
\mforall{}[A:Type]
\mforall{}R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}as,bs:A  List.
(StAntiSym(A;x,y.\muparrow{}R[x;y])
{}\mRightarrow{}  Irrefl(A;x,y.\muparrow{}R[x;y])
{}\mRightarrow{}  Trans(A;x,y.\muparrow{}R[x;y])
{}\mRightarrow{}  no\_repeats(A;as)
{}\mRightarrow{}  l-ordered(A;x,y.\muparrow{}R[x;y];as)
{}\mRightarrow{}  l-ordered(A;x,y.\muparrow{}R[x;y];bs)
{}\mRightarrow{}  (\mforall{}a\mmember{}as.(a  \mmember{}  bs))
{}\mRightarrow{}  as  \msubseteq{}  bs)

Date html generated: 2016_10_25-AM-10_57_32
Last ObjectModification: 2016_07_12-AM-07_05_08

Theory : general

Home Index