### Nuprl Lemma : mon_when_when

`∀[g:Mon]. ∀[b,b':𝔹]. ∀[p:|g|].  ((when b. when b'. p) = (when b ∧b b'. p) ∈ |g|)`

Proof

Definitions occuring in Statement :  mon_when: `when b. p` mon: `Mon` grp_car: `|g|` band: `p ∧b q` bool: `𝔹` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` mon_when: `when b. p` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` band: `p ∧b q` bfalse: `ff` mon: `Mon`
Lemmas referenced :  grp_id_wf grp_car_wf bool_wf mon_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution unionElimination thin equalityElimination sqequalRule hypothesisEquality lemma_by_obid isectElimination setElimination rename hypothesis because_Cache isect_memberEquality axiomEquality

Latex:
\mforall{}[g:Mon].  \mforall{}[b,b':\mBbbB{}].  \mforall{}[p:|g|].    ((when  b.  when  b'.  p)  =  (when  b  \mwedge{}\msubb{}  b'.  p))

Date html generated: 2016_05_15-PM-00_18_50
Last ObjectModification: 2015_12_26-PM-11_37_57

Theory : groups_1

Home Index