Nuprl Definition : seq-adjoin
s++t == seq-append(n;1;s;λi.t)
Definitions occuring in Statement :
seq-append: seq-append(n;m;s1;s2),
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
seq-append: seq-append(n;m;s1;s2),
natural_number: $n,
lambda: λx.A[x]
FDL editor aliases :
seq-adjoin
Latex:
s++t == seq-append(n;1;s;\mlambda{}i.t)
Date html generated:
2016_05_13-PM-03_49_15
Last ObjectModification:
2015_09_22-PM-05_45_18
Theory : bar-induction
Home
Index