Nuprl Definition : permr_massoc
as ≡ bs upto ~ == as ≡ bs upto x,y.x ~ y
Definitions occuring in Statement :
massoc: a ~ b,
permr_upto: as ≡ bs upto x,y.R[x; y]
Definitions occuring in definition :
permr_upto: as ≡ bs upto x,y.R[x; y] ,
massoc: a ~ b
Latex:
as \mequiv{} bs upto \msim{} == as \mequiv{} bs upto x,y.x \msim{} y
Date html generated:
2016_05_16-AM-07_44_38
Last ObjectModification:
2015_09_23-AM-09_51_55
Theory : factor_1
Home
Index