Nuprl Lemma : nat_add_mon_wf2
<ℕ,+> ∈ OCMon
Proof
Definitions occuring in Statement :
nat_add_mon: <ℕ,+>,
ocmon: OCMon,
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
exists: ∃x:A. B[x],
and: P ∧ Q,
prop: ℙ,
subtype_rel: A ⊆r B,
nat_add_mon: <ℕ,+>,
grp_car: |g|,
pi1: fst(t),
int_add_grp: <ℤ+>,
nat: ℕ,
rels_iso: RelsIso(T;T';x,y.R[x; y];x,y.R'[x; y];f),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
grp_eq: =b,
pi2: snd(t),
infix_ap: x f y,
rev_implies: P ⇐ Q,
grp_le: ≤b,
guard: {T},
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
ocmon: OCMon,
abmonoid: AbMon,
mon: Mon,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
inj_into_ocmon,
nat_add_mon_wf,
int_add_grp_wf2,
ocgrp_subtype_ocmon,
nat_wf,
nat_int_grp_sig_hom,
assert_wf,
eq_int_wf,
le_int_wf,
mon_hom_inj_p_wf,
int_add_grp_wf,
mon_subtype_grp_sig,
grp_subtype_mon,
abgrp_subtype_grp,
subtype_rel_transitivity,
abgrp_wf,
grp_wf,
mon_wf,
grp_sig_wf,
rels_iso_wf,
grp_car_wf,
grp_eq_wf,
grp_le_wf,
exists_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesis,
independent_isectElimination,
dependent_pairFormation,
independent_pairFormation,
applyEquality,
sqequalRule,
lambdaEquality,
setElimination,
rename,
hypothesisEquality,
lambdaFormation,
because_Cache,
productEquality,
instantiate,
functionEquality
Latex:
<\mBbbN{},+> \mmember{} OCMon
Date html generated:
2018_05_21-PM-03_14_08
Last ObjectModification:
2018_05_19-AM-08_26_05
Theory : groups_1
Home
Index