Nuprl Lemma : es-init-elim2

[es:EO]. ∀[e:E].  es-init(es;e) es-init(es;pred(e)) supposing ¬↑first(e)


Proof




Definitions occuring in Statement :  es-init: es-init(es;e) es-first: first(e) es-pred: pred(e) es-E: E event_ordering: EO assert: b uimplies: supposing a uall: [x:A]. B[x] not: ¬A sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a es-init: es-init(es;e) final-iterate: final-iterate(f;x) do-apply: do-apply(f;x) can-apply: can-apply(f;x) all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  not: ¬A false: False bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b isl: isl(x) outl: outl(x)

Latex:
\mforall{}[es:EO].  \mforall{}[e:E].    es-init(es;e)  \msim{}  es-init(es;pred(e))  supposing  \mneg{}\muparrow{}first(e)



Date html generated: 2016_05_16-AM-09_39_50
Last ObjectModification: 2015_12_28-PM-09_43_18

Theory : new!event-ordering


Home Index