Nuprl Definition : count
a #∈ as == For{<ℤ+>} x ∈ as. b2i(x (=b) a)
Wellformedness Lemmas :
count_wf
Definitions occuring in Statement :
mon_for: For{g} x ∈ as. f[x],
b2i: b2i(b),
infix_ap: x f y,
int_add_grp: <ℤ+>,
set_eq: =b,
set_car: |p|
Definitions occuring in definition :
mon_for: For{g} x ∈ as. f[x],
set_car: |p|,
int_add_grp: <ℤ+>,
b2i: b2i(b),
infix_ap: x f y,
set_eq: =b
Latex:
a \#\mmember{} as == For\{<\mBbbZ{}+>\} x \mmember{} as. b2i(x (=\msubb{}) a)
Date html generated:
2016_05_16-AM-07_39_21
Last ObjectModification:
2015_09_23-AM-09_51_38
Theory : list_2
Home
Index