Nuprl Lemma : max-fst-property
∀[Info,A,T:Type].
∀es:EO+(Info). ∀X:EClass(T × A). ∀e:E.
{(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (T × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))}
supposing ↑e ∈b MaxFst(X)
supposing T ⊆r ℤ
Proof
Definitions occuring in Statement :
max-fst-class: MaxFst(X),
es-interface-predecessors: ≤(X)(e),
es-E-interface: E(X),
eclass-val: X(e),
in-eclass: e ∈b X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-le: e ≤loc e' ,
es-E: E,
imax-list: imax-list(L),
map: map(f;as),
assert: ↑b,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
guard: {T},
pi1: fst(t),
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
lambda: λx.A[x],
product: x:A × B[x],
int: ℤ,
universe: Type,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
guard: {T},
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uimplies: b supposing a,
prop: ℙ,
subtype_rel: A ⊆r B,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
and: P ∧ Q,
cand: A c∧ B,
nat: ℕ,
false: False,
ge: i ≥ j ,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
not: ¬A,
top: Top,
or: P ∨ Q,
pi1: fst(t),
cons: [a / b],
colength: colength(L),
decidable: Dec(P),
nil: [],
it: ⋅,
so_lambda: λ2x.t[x],
so_apply: x[s],
sq_type: SQType(T),
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
es-E-interface: E(X),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
bool: 𝔹,
unit: Unit,
uiff: uiff(P;Q),
bfalse: ff,
bnot: ¬bb,
le: A ≤ B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
imax-list: imax-list(L),
accum_list: accum_list(a,x.f[a; x];x.base[x];L),
combine-list: combine-list(x,y.f[x; y];L),
subtract: n - m,
sq_stable: SqStable(P),
pi2: snd(t)
Latex:
\mforall{}[Info,A,T:Type].
\mforall{}es:EO+(Info). \mforall{}X:EClass(T \mtimes{} A). \mforall{}e:E.
\{(fst(MaxFst(X)(e)) \msim{} imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e))))
\mwedge{} (\mexists{}mxe:E(X)
(mxe \mleq{}loc e
\mwedge{} (MaxFst(X)(e) = X(mxe))
\mwedge{} (\mforall{}e':E(X). (e' \mleq{}loc e {}\mRightarrow{} ((fst(X(e'))) \mleq{} (fst(X(mxe))))))))\}
supposing \muparrow{}e \mmember{}\msubb{} MaxFst(X)
supposing T \msubseteq{}r \mBbbZ{}
Date html generated:
2016_05_17-AM-07_03_36
Last ObjectModification:
2016_01_17-PM-07_36_52
Theory : event-ordering
Home
Index