Nuprl Lemma : assert-exists_sublist

[T:Type]. ∀L:T List. ∀P:(T List) ⟶ 𝔹.  (↑exists_sublist(L;P) ⇐⇒ ∃LL:T List. (LL ⊆ L ∧ (↑(P LL))))


Proof




Definitions occuring in Statement :  exists_sublist: exists_sublist(L;P) sublist: L1 ⊆ L2 list: List assert: b bool: 𝔹 uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q apply: a 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] prop: and: P ∧ Q so_apply: x[s] implies:  Q exists_sublist: exists_sublist(L;P) ifthenelse: if then else fi  btrue: tt top: Top so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] bfalse: ff iff: ⇐⇒ Q exists: x:A. B[x] cand: c∧ B rev_implies:  Q uimplies: supposing a guard: {T} uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) or: P ∨ Q cons: [a b] sq_type: SQType(T) assert: b true: True
Lemmas referenced :  list_induction all_wf list_wf bool_wf iff_wf assert_wf exists_sublist_wf exists_wf sublist_wf null_nil_lemma null_cons_lemma spread_cons_lemma nil_wf nil-sublist assert_witness sublist_nil assert_functionality_wrt_uiff or_wf cons_wf assert_of_bor bor_wf sublist_tl2 cons_sublist_cons list-cases product_subtype_list and_wf equal_wf assert_elim subtype_base_sq bool_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality cumulativity hypothesis functionExtensionality applyEquality productEquality independent_functionElimination rename dependent_functionElimination isect_memberEquality voidElimination voidEquality because_Cache universeEquality independent_pairFormation dependent_pairFormation productElimination independent_isectElimination equalitySymmetry unionElimination addLevel allFunctionality impliesFunctionality orFunctionality orLevelFunctionality inlFormation promote_hyp hypothesis_subsumption inrFormation dependent_set_memberEquality applyLambdaEquality setElimination equalityTransitivity levelHypothesis instantiate natural_numberEquality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}P:(T  List)  {}\mrightarrow{}  \mBbbB{}.    (\muparrow{}exists\_sublist(L;P)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}LL:T  List.  (LL  \msubseteq{}  L  \mwedge{}  (\muparrow{}(P  LL))))



Date html generated: 2018_05_21-PM-00_34_15
Last ObjectModification: 2017_10_12-AM-10_13_20

Theory : list_1


Home Index