Nuprl Lemma : rng_lookup_before_start

`∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps:|omral(g;r)|.  ((↑before(k;map(λz.(fst(z));ps))) `` ((ps[k]) = 0 ∈ |r|))`

Proof

Definitions occuring in Statement :  omralist: `omral(g;r)` lookup: `as[k]` before: `before(u;ps)` map: `map(f;as)` assert: `↑b` pi1: `fst(t)` all: `∀x:A. B[x]` implies: `P `` Q` lambda: `λx.A[x]` equal: `s = t ∈ T` cdrng: `CDRng` rng_zero: `0` rng_car: `|r|` oset_of_ocmon: `g↓oset` ocmon: `OCMon` grp_car: `|g|` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` ocmon: `OCMon` omon: `OMon` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` abmonoid: `AbMon` mon: `Mon` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` uimplies: `b supposing a` bfalse: `ff` infix_ap: `x f y` so_apply: `x[s]` cand: `A c∧ B` oset_of_ocmon: `g↓oset` dset_of_mon: `g↓set` set_car: `|p|` pi1: `fst(t)` add_grp_of_rng: `r↓+gp` grp_car: `|g|` grp_id: `e` pi2: `snd(t)` omralist: `omral(g;r)`
Lemmas referenced :  lookup_before_start oset_of_ocmon_wf subtype_rel_sets abmonoid_wf ulinorder_wf grp_car_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf grp_eq_wf eqtt_to_assert cancel_wf grp_op_wf uall_wf monot_wf cdrng_wf ocmon_wf cdrng_is_abdmonoid
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality applyEquality sqequalRule instantiate hypothesis because_Cache lambdaEquality productEquality setElimination rename cumulativity universeEquality functionEquality unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination setEquality independent_pairFormation

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}k:|g|.  \mforall{}ps:|omral(g;r)|.    ((\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps)))  {}\mRightarrow{}  ((ps[k])  =  0))

Date html generated: 2017_10_01-AM-10_05_05
Last ObjectModification: 2017_03_03-PM-01_10_16

Theory : polynom_3

Home Index