Nuprl Definition : finite-fun-deq

finite-fun-deq(k;eq) ==  λf,g. bdd-all(k;i.eq (f i) (g i))


Definitions occuring in Statement :  bdd-all: bdd-all(n;i.P[i]),  apply: f a,  lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x],  bdd-all: bdd-all(n;i.P[i]),  apply: f a
FDL editor aliases :  finite-fun-deq
Latex:
finite-fun-deq(k;eq)  ==    \mlambda{}f,g.  bdd-all(k;i.eq  (f  i)  (g  i))


Date html generated: 2020_05_19-PM-09_36_34
Last ObjectModification: 2019_10_18-AM-11_55_33

Theory : equality!deciders


Home Index