{ 
[Info:Type]
es:EO+(Info). Sys:EClass(Top). f:sys-antecedent(es;Sys). x,y:E(Sys).
i:Id.
x-f*-y thru i 
x-f*-y goes thru i last supposing 
(loc(x) = i) }
{ Proof }
Definitions occuring in Statement :
path-goes-thru-last: x-f*-y goes thru i last,
path-goes-thru: x-f*-y thru i,
sys-antecedent: sys-antecedent(es;Sys),
es-E-interface: E(X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-loc: loc(e),
Id: Id,
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
not: A,
implies: P Q,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
uimplies: b supposing a,
not: A,
implies: P Q,
member: t 
T,
false: False,
prop: 
,
so_lambda: 
x y.t[x; y],
path-goes-thru-last: x-f*-y goes thru i last,
Id: Id,
exists: 
x:A. B[x],
and: P 
Q,
cand: A c B,
sys-antecedent: sys-antecedent(es;Sys),
es-E-interface: E(X),
so_apply: x[s1;s2],
path-goes-thru: x-f*-y thru i,
sq_type: SQType(T),
guard: {T},
subtype: S 
T
Lemmas :
Id_wf,
es-loc_wf,
path-goes-thru_wf,
not_wf,
es-E-interface_wf,
sys-antecedent_wf,
eclass_wf,
top_wf,
es-E_wf,
event-ordering+_wf,
chain-pullback,
subtype_base_sq,
atom2_subtype_base,
fun-connected_transitivity,
event-ordering+_inc,
es-E-interface-subtype_rel,
fun-connected_wf
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}Sys:EClass(Top). \mforall{}f:sys-antecedent(es;Sys). \mforall{}x,y:E(Sys). \mforall{}i:Id.
x-f*-y thru i {}\mRightarrow{} x-f*-y goes thru i last supposing \mneg{}(loc(x) = i)
Date html generated:
2011_08_16-PM-06_02_47
Last ObjectModification:
2011_06_20-AM-01_46_06
Home
Index