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:
2019_06_20-PM-00_56_21
Last ObjectModification:
2019_01_02-PM-01_33_11
Theory : co-recursion-2
Home
Index