Nuprl Lemma : iseg-transition-lemma

[T:Type]. ∀[P:(T List) ⟶ ℙ].
  ∀L:T List. ∀x:T.
    ((∃L1:T List. (L1 ≤ [x] ∧ P[L1])) ∧ (∃L1:T List. (L1 ≤ L ∧ P[L1])))
    ⇐⇒ P[L [x]] ∧ (∃L1:T List. (L1 ≤ L ∧ P[L1]))))


Proof




Definitions occuring in Statement :  iseg: l1 ≤ l2 append: as bs cons: [a b] nil: [] list: List uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q not: ¬A and: P ∧ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q not: ¬A false: False member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B exists: x:A. B[x] rev_implies:  Q cand: c∧ B or: P ∨ Q squash: T true: True less_than: a < b less_than': less_than'(a;b) cons: [a b] top: Top assert: b ifthenelse: if then else fi  btrue: tt bfalse: ff
Lemmas referenced :  exists_wf list_wf iseg_wf append_wf cons_wf nil_wf not_wf iseg_weakening iseg_append_iff equal_wf list-cases length_of_nil_lemma product_subtype_list length_of_cons_lemma cons_iseg iseg_nil null_nil_lemma null_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation sqequalHypSubstitution productElimination thin cut hypothesis independent_functionElimination voidElimination introduction extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule lambdaEquality productEquality applyEquality functionExtensionality universeEquality because_Cache dependent_pairFormation dependent_functionElimination functionEquality unionElimination addLevel hyp_replacement equalitySymmetry levelHypothesis imageElimination natural_numberEquality imageMemberEquality baseClosed Error :applyLambdaEquality,  promote_hyp hypothesis_subsumption isect_memberEquality voidEquality rename

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L:T  List.  \mforall{}x:T.
        ((\mexists{}L1:T  List.  (L1  \mleq{}  L  @  [x]  \mwedge{}  P[L1]))  \mwedge{}  (\mneg{}(\mexists{}L1:T  List.  (L1  \mleq{}  L  \mwedge{}  P[L1])))
        \mLeftarrow{}{}\mRightarrow{}  P[L  @  [x]]  \mwedge{}  (\mneg{}(\mexists{}L1:T  List.  (L1  \mleq{}  L  \mwedge{}  P[L1]))))



Date html generated: 2016_10_25-AM-10_54_48
Last ObjectModification: 2016_07_12-AM-07_02_05

Theory : general


Home Index