Nuprl Definition : Maximal_order_type
Maximal_order_type() ==
λx.let A,<,x3,x4 = x
in <λa.<b:A × (< b a), λp1,p2. (< (fst(p1)) (fst(p2))), λf,%. Ax>, <A, <, x3>, λa1,a2,%. <λp1.let a,p2 = p1 in <a, \000Cx4 a a1 a2 p2 %>, <a1, %>, λa1@0,a2,%. %, λa.(snd(a))>, λa.<λx.(fst(x)), a, λa1,a2,%. %, λa.(snd(a))>>
Definitions occuring in Statement :
spreadn: spread4,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
product: x:A × B[x],
axiom: Ax
Definitions occuring in definition :
pi2: snd(t),
lambda: λx.A[x],
pair: <a, b>,
pi1: fst(t),
apply: f a,
spread: spread def,
axiom: Ax,
product: x:A × B[x],
spreadn: spread4
FDL editor aliases :
Maximal_order_type
Latex:
Maximal\_order\_type() ==
\mlambda{}x.let A,<,x3,x4 = x
in <\mlambda{}a.<b:A \mtimes{} (< b a), \mlambda{}p1,p2. (< (fst(p1)) (fst(p2))), \mlambda{}f,\%. Ax>, <A, <, x3>, \mlambda{}a1,a2,\%. <\mlambda{}p1.l\000Cet a,p2 = p1 in <a, x4 a a1 a2 p2 \%>, <a1, \%>, \mlambda{}a1@0,a2,\%. \%, \mlambda{}a.(snd(a))>, \mlambda{}a.<\mlambda{}x.(fst(x)), a, \mlambda{}a1,\000Ca2,\%. \%, \mlambda{}a.(snd(a))>>
Date html generated:
2018_05_21-PM-07_15_11
Last ObjectModification:
2018_05_18-AM-08_14_43
Theory : general
Home
Index