Nuprl Definition : nysiad_Amessage-deq
nysiad_Amessage-deq(M;deqM) == product-deq(M;Id? × Id;deqM;product-deq(Id?;Id;union-deq(Id;Unit;IdDeq;UnitDeq);IdDeq))
Definitions occuring in Statement :
id-deq: IdDeq,
Id: Id,
union-deq: union-deq(A;B;a;b),
product-deq: product-deq(A;B;a;b),
unit-deq: UnitDeq,
unit: Unit,
product: x:A × B[x],
union: left + right
FDL editor aliases :
nysiad_Amessage-deq
Latex:
nysiad\_Amessage-deq(M;deqM) ==
product-deq(M;Id? \mtimes{} Id;deqM;product-deq(Id?;Id;union-deq(Id;Unit;IdDeq;UnitDeq);IdDeq))
Date html generated:
2015_07_23-PM-03_43_00
Last ObjectModification:
2014_08_06-PM-03_29_21
Home
Index