EO ==
"E":Type
"dom":self."E" 
"<":self."E" self."E" 
"loc":self."E" Id
"deq":
e1,e2:self."E". ((e1 = e2) 
(
(e1 = e2)))
"wf":
f:self."E" 
. x,y:self."E". ((x self."<" y) 
((f x) < (f y)))
"dco":e1,e2:self."E". ((e1 self."<" e2) ((e1 self."<" e2)))
"trans":x,y,z:self."E". ((x self."<" y) (y self."<" z) (x self."<" z))
"fin":x:self."E". L:self."E" List. z:self."E". ((z self."<" x) (z 
L))
"total":e1,e2:self."E".
(e1 = e2) (e1 self."<" e2) (e2 self."<" e1)
supposing (self."loc" e1) = (self."loc" e2)
Definitions occuring in Statement :
Id: Id,
bool: ,
nat: ,
uimplies: b supposing a,
top: Top,
prop: ,
infix_ap: x f y,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
or: P Q,
less_than: a < b,
apply: f a,
function: x:A B[x],
list: type List,
token: "$token",
universe: Type,
equal: s = t,
l_member: (x l),
record-select: r.x,
record+: record+,
record: record(x.T[x])
Definitions :
record-select: r.x,
infix_ap: x f y,
token: "$token",
implies: P Q,
all: x:A. B[x],
not: A,
or: P Q,
apply: f a,
less_than: a < b,
nat: ,
function: x:A B[x],
exists: x:A. B[x],
equal: s = t,
Id: Id,
prop: ,
bool: ,
universe: Type,
top: Top,
record: record(x.T[x]),
record+: record+,
list: type List,
l_member: (x l),
uimplies: b supposing a
FDL editor aliases :
EO
EO ==
"E":Type
"dom":self."E" {}\mrightarrow{} \mBbbB{}
"<":self."E" {}\mrightarrow{} self."E" {}\mrightarrow{} \mBbbP{}
"loc":self."E" {}\mrightarrow{} Id
"deq":\mforall{}e1,e2:self."E". ((e1 = e2) \mvee{} (\mneg{}(e1 = e2)))
"wf":\mexists{}f:self."E" {}\mrightarrow{} \mBbbN{}. \mforall{}x,y:self."E". ((x self."<" y) {}\mRightarrow{} ((f x) < (f y)))
"dco":\mforall{}e1,e2:self."E". ((e1 self."<" e2) \mvee{} (\mneg{}(e1 self."<" e2)))
"trans":\mforall{}x,y,z:self."E". ((x self."<" y) {}\mRightarrow{} (y self."<" z) {}\mRightarrow{} (x self."<" z))
"fin":\mforall{}x:self."E". \mexists{}L:self."E" List. \mforall{}z:self."E". ((z self."<" x) {}\mRightarrow{} (z \mmember{} L))
"total":\mforall{}e1,e2:self."E".
(e1 = e2) \mvee{} (e1 self."<" e2) \mvee{} (e2 self."<" e1)
supposing (self."loc" e1) = (self."loc" e2)
Date html generated:
2011_08_16-AM-10_19_21
Last ObjectModification:
2010_11_22-PM-03_16_01
Home
Index