Nuprl Lemma : sub-bag-admissable

[T:Type]. ∀[R:bag(T) ⟶ bag(T) ⟶ ℙ].
  (bag-admissable(T;as,bs.R[as;bs])  (∀as,bs:bag(T).  (sub-bag(T;as;bs)  R[as;bs])))


Proof




Definitions occuring in Statement :  bag-admissable: bag-admissable(T;as,bs.R[as; bs]) sub-bag: sub-bag(T;as;bs) bag: bag(T) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] sub-bag: sub-bag(T;as;bs) exists: x:A. B[x] bag-admissable: bag-admissable(T;as,bs.R[as; bs]) and: P ∧ Q member: t ∈ T prop: so_apply: x[s1;s2] so_lambda: λ2y.t[x; y] guard: {T} top: Top squash: T true: True subtype_rel: A ⊆B uimplies: supposing a iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  equal_wf bag_wf sub-bag_wf bag-admissable_wf empty-bag_wf bag-empty-append squash_wf true_wf bag-append-comm bag-append_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin cut hypothesis equalitySymmetry hyp_replacement applyLambdaEquality introduction extract_by_obid isectElimination cumulativity hypothesisEquality equalityTransitivity applyEquality functionExtensionality sqequalRule lambdaEquality functionEquality universeEquality dependent_functionElimination independent_functionElimination isect_memberEquality voidElimination voidEquality imageElimination because_Cache natural_numberEquality imageMemberEquality baseClosed independent_isectElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:bag(T)  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  \mBbbP{}].
    (bag-admissable(T;as,bs.R[as;bs])  {}\mRightarrow{}  (\mforall{}as,bs:bag(T).    (sub-bag(T;as;bs)  {}\mRightarrow{}  R[as;bs])))



Date html generated: 2017_10_01-AM-09_05_09
Last ObjectModification: 2017_07_26-PM-04_45_06

Theory : bags


Home Index