### Nuprl Lemma : assert-exists-l_subset

`∀[T:Type]`
`  ((∀x,y:T.  Dec(x = y ∈ T))`
`  `` (∀P:(T List) ⟶ 𝔹`
`        ((∀L1,L2:T List.  (set-equal(T;L1;L2) `` (↑(P L1) `⇐⇒` ↑(P L2))))`
`        `` (∀L:T List. (↑exists_sublist(L;P) `⇐⇒` ∃LL:T List. (l_subset(T;LL;L) ∧ (↑(P LL))))))))`

Proof

Definitions occuring in Statement :  set-equal: `set-equal(T;x;y)` l_subset: `l_subset(T;as;bs)` exists_sublist: `exists_sublist(L;P)` list: `T List` assert: `↑b` bool: `𝔹` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rev_implies: `P `` Q` exists: `∃x:A. B[x]` cand: `A c∧ B` l_subset: `l_subset(T;as;bs)` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` false: `False` set-equal: `set-equal(T;x;y)`
Lemmas referenced :  exists_wf list_wf sublist_wf assert_wf l_subset_wf assert-exists_sublist exists_sublist_wf all_wf iff_wf set-equal_wf bool_wf decidable_wf equal_wf l_member_wf member_sublist list_induction nil_wf cons_wf l_subset_nil_right sublist_nil set-equal-reflex decidable__l_member deq-exists list-diff_wf cons_member member_singleton not_wf member-list-diff cons_sublist_cons or_wf and_wf sublist_tl2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut independent_pairFormation introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis sqequalRule lambdaEquality productEquality applyEquality functionExtensionality addLevel allFunctionality productElimination impliesFunctionality dependent_functionElimination independent_functionElimination because_Cache functionEquality universeEquality dependent_pairFormation promote_hyp rename unionElimination andLevelFunctionality impliesLevelFunctionality voidElimination inlFormation levelHypothesis hyp_replacement equalitySymmetry dependent_set_memberEquality applyLambdaEquality setElimination inrFormation

Latex:
\mforall{}[T:Type]
((\mforall{}x,y:T.    Dec(x  =  y))
{}\mRightarrow{}  (\mforall{}P:(T  List)  {}\mrightarrow{}  \mBbbB{}
((\mforall{}L1,L2:T  List.    (set-equal(T;L1;L2)  {}\mRightarrow{}  (\muparrow{}(P  L1)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(P  L2))))
{}\mRightarrow{}  (\mforall{}L:T  List.  (\muparrow{}exists\_sublist(L;P)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}LL:T  List.  (l\_subset(T;LL;L)  \mwedge{}  (\muparrow{}(P  LL))))))))

Date html generated: 2018_05_21-PM-00_51_28
Last ObjectModification: 2017_10_12-AM-10_50_37

Theory : decidable!equality

Home Index