Nuprl - mb_declaration Citations of eq

Def l1 =

l2 == Case(l1) Case ptn_atom(x) = > Case(l2) Case ptn_atom(y) = > x=

Atom Default = > false

Case ptn_int(x) = > Case(l2) Case ptn_int(y) = > x=

y Default = > false

Case ptn_var(x) = > Case(l2) Case ptn_var(y) = > x=

Atom Default = > false

Case ptn_pr( < x, y > ) = > Case(l2) Case ptn_pr( < u, v > ) = > x =

y =

v Default = > false

Default = > false

(recursive)

is mentioned by

Def d o f(x) == y:Label. if x = f(y) d(y) else Top fi [rename_decl]

Def x:y(a) == if a = x y else Top fi [dbase]

In prior sections: mb basic mb label

Try larger context: GenAutomata

`Def d o f(x) == y:Label. if x = f(y) d(y) else Top fi`	[rename_decl]
`Def x:y(a) == if a = x y else Top fi`	[dbase]