Nuprl - mb automata 2 Citations of case relname eq

Def Case eq(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))

is mentioned by

Def [[rn]] rho e == Case(rn) Case eq(Q) = > x,y. x = y [[Q]] rho Case R = > e.R Default = > True [relname_mng]

Def eq_relname(a;b) == Case(a) Case eq(x) = > Case(b) Case eq(x') = > st_eq(x;x') Case x' = > false Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x = x' Default = > false Default = > false [eq_relname]

In prior sections: mb automata 1

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc

`Def [[rn]] rho e == Case(rn) Case eq(Q) = > x,y. x = y [[Q]] rho Case R = > e.R Default = > True`	[relname_mng]
`Def eq_relname(a;b) == Case(a) Case eq(x) = > Case(b) Case eq(x') = > st_eq(x;x') Case x' = > false Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x = x' Default = > false Default = > false`	[eq_relname]