Nuprl Definition : copath
copath(a.B[a];w) ==  n:ℕ × coPath(a.B[a];w;n)
Definitions occuring in Statement : 
coPath: coPath(a.B[a];w;n)
, 
nat: ℕ
, 
product: x:A × B[x]
Definitions occuring in definition : 
product: x:A × B[x]
, 
nat: ℕ
, 
coPath: coPath(a.B[a];w;n)
FDL editor aliases : 
copath
Latex:
copath(a.B[a];w)  ==    n:\mBbbN{}  \mtimes{}  coPath(a.B[a];w;n)
Date html generated:
2018_07_25-PM-01_38_46
Last ObjectModification:
2018_06_01-AM-08_31_32
Theory : co-recursion
Home
Index