Nuprl Lemma : simple-comb-2-es-sv
∀[Info,A,B,C:Type]. ∀[es:EO+(Info)]. ∀[F:A ─→ B ─→ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
(es-sv-class(es;lifting-2(F)|X, Y|)) supposing (es-sv-class(es;Y) and es-sv-class(es;X))
Proof
Definitions occuring in Statement :
simple-comb-2: F|X, Y|,
es-sv-class: es-sv-class(es;X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
function: x:A ─→ B[x],
universe: Type,
lifting-2: lifting-2(f)
Lemmas :
false_wf,
lelt_wf,
bag-size_wf,
select_wf,
cons_wf,
nil_wf,
length_wf,
length_nil,
non_neg_length,
length_wf_nil,
length_cons,
length_wf_nat,
nat_wf,
bag-size-zero,
bag_wf,
le_weakening,
bag-combine-empty-left,
bag-size-one,
length_of_cons_lemma,
length_of_nil_lemma,
bag-combine-single-left,
bag-only_wf2,
single-valued-bag-if-le1,
decidable__lt,
le_antisymmetry_iff,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
bag-combine_wf,
single-bag_wf,
add-commutes,
zero-add,
bag_size_single_lemma,
le_wf,
squash_wf,
true_wf,
iff_weakening_equal
Latex:
\mforall{}[Info,A,B,C:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[F:A {}\mrightarrow{} B {}\mrightarrow{} C]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)].
(es-sv-class(es;lifting-2(F)|X, Y|)) supposing (es-sv-class(es;Y) and es-sv-class(es;X))
Date html generated:
2015_07_22-PM-00_16_20
Last ObjectModification:
2015_02_04-PM-04_40_55
Home
Index