Nuprl Definition : deq-all-disjoint

deq-all-disjoint(eq;ass;bs) ==  (∀as∈ass.deq-disjoint(eq;as;bs))_b


Definitions occuring in Statement :  deq-disjoint: deq-disjoint(eq;as;bs),  bl-all: (∀x∈L.P[x])_b
Definitions occuring in definition :  bl-all: (∀x∈L.P[x])_b,  deq-disjoint: deq-disjoint(eq;as;bs)
FDL editor aliases :  deq-all-disjoint
Latex:
deq-all-disjoint(eq;ass;bs)  ==    (\mforall{}as\mmember{}ass.deq-disjoint(eq;as;bs))\_b


Date html generated: 2016_05_14-PM-03_24_05
Last ObjectModification: 2015_09_22-PM-05_59_32

Theory : decidable!equality


Home Index