Nuprl Definition : union-ss
ss1 + ss2 ==
Point=Point(ss1) + Point(ss2) #=λp,q. union-sep(ss1;ss2;p;q) cotrans=λx,y,z,sep. case x
of inl(a) =>
case y
of inl(a') =>
case z
of inl(a'') =>
ss1."#or" a a' a'' sep
| inr(_) =>
inl Ax
| inr(b') =>
case z
of inl(_) =>
inr Ax
| inr(_) =>
inl Ax
| inr(b) =>
case y
of inl(a') =>
case z
of inl(_) =>
inl Ax
| inr(_) =>
inr Ax
| inr(b') =>
case z
of inl(_) =>
inl Ax
| inr(b'') =>
ss2."#or" b b' b'' sep
Definitions occuring in Statement :
union-sep: union-sep(ss1;ss2;p;q),
mk-ss: Point=P #=Sep cotrans=C,
ss-point: Point(ss),
apply: f a,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
union: left + right,
token: "$token",
axiom: Ax,
record-select: r.x
Definitions occuring in definition :
mk-ss: Point=P #=Sep cotrans=C,
union: left + right,
ss-point: Point(ss),
union-sep: union-sep(ss1;ss2;p;q),
lambda: λx.A[x],
inr: inr x ,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
axiom: Ax,
apply: f a,
record-select: r.x,
token: "$token"
FDL editor aliases :
union-ss
Latex:
ss1 + ss2 ==
Point=Point(ss1) + Point(ss2) \#=\mlambda{}p,q. union-sep(ss1;ss2;p;q) cotrans=\mlambda{}x,y,z,sep. case x
of inl(a) =>
case y
of inl(a') =>
case z
of inl(a'') =>
ss1."\#or" a a' a''
sep
| inr($_\mbackslash{}ff\000C7b}$) =>
inl Ax
| inr(b') =>
case z
of inl($_\mbackslash{}f\000Cf7b}$) =>
inr Ax
| inr($_\mbackslash{}ff\000C7b}$) =>
inl Ax
| inr(b) =>
case y
of inl(a') =>
case z
of inl($_\mbackslash{}f\000Cf7b}$) =>
inl Ax
| inr($_\mbackslash{}ff\000C7b}$) =>
inr Ax
| inr(b') =>
case z
of inl($_\mbackslash{}f\000Cf7b}$) =>
inl Ax
| inr(b'') =>
ss2."\#or" b b' b''
sep
Date html generated:
2019_10_31-AM-07_27_00
Last ObjectModification:
2019_09_19-PM-04_10_46
Theory : constructive!algebra
Home
Index