### Nuprl Lemma : simple-comb-4_wf

`∀[Info,A,B,C,D,E:Type].`
`  ∀F:bag(A) ─→ bag(B) ─→ bag(C) ─→ bag(D) ─→ bag(E)`
`    ∀[W:EClass(A)]. ∀[X:EClass(B)]. ∀[Y:EClass(C)]. ∀[Z:EClass(D)].  (simple-comb-4(F;W;X;Y;Z) ∈ EClass(E))`

Proof

Definitions occuring in Statement :  simple-comb-4: `simple-comb-4(F;W;X;Y;Z)` eclass: `EClass(A[eo; e])` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` function: `x:A ─→ B[x]` universe: `Type` bag: `bag(T)`
Lemmas :  simple-comb_wf false_wf le_wf select_wf cons_wf nil_wf sq_stable__le length_wf length_nil non_neg_length length_wf_nil length_cons length_wf_nat int_seg_wf decidable__equal_int subtype_base_sq int_subtype_base lelt_wf bag_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf

Latex:
\mforall{}[Info,A,B,C,D,E:Type].
\mforall{}F:bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)  {}\mrightarrow{}  bag(D)  {}\mrightarrow{}  bag(E)
\mforall{}[W:EClass(A)].  \mforall{}[X:EClass(B)].  \mforall{}[Y:EClass(C)].  \mforall{}[Z:EClass(D)].
(simple-comb-4(F;W;X;Y;Z)  \mmember{}  EClass(E))

Date html generated: 2015_07_21-PM-03_02_16
Last ObjectModification: 2015_01_29-PM-08_20_31

Home Index