### Nuprl Lemma : bag-admissable_wf

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

Proof

Definitions occuring in Statement :  bag-admissable: bag-admissable(T;as,bs.R[as; bs]) bag: bag(T) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag-admissable: bag-admissable(T;as,bs.R[as; bs]) prop: and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] implies:  Q subtype_rel: A ⊆B
Lemmas referenced :  all_wf bag_wf empty-bag_wf bag-append_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule productEquality lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis lambdaEquality applyEquality because_Cache functionEquality universeEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

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

Date html generated: 2016_05_15-PM-03_10_33
Last ObjectModification: 2015_12_27-AM-09_25_16

Theory : bags

Home Index