Nuprl - mb automata 2 Citations of case node

Def Case x;y = > body(x;y) cont(x1,z) == InjCase(x1; _. cont(z,z); x2. x2/x3,x2@0. body(x3;x2@0))

is mentioned by

Def st_app1(s1;s2) == Case(s1) Case a;b = > if st_eq(a;s2) < b > else < > fi Default = > < > [st_app1]

Def term_eq(a;b) == Case(a) Case x;y = > Case(b) Case x';y' = > term_eq(x;x')term_eq(y;y') Case tree_leaf(x) = > false Default = > True Case tree_leaf(x) = > Case(b) Case x';y' = > false Case tree_leaf(x') = > (x=x') Default = > True Default = > True (recursive) [term_eq]

In prior sections: mb tree mb automata 1

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc

`Def st_app1(s1;s2) == Case(s1) Case a;b = > if st_eq(a;s2) < b > else < > fi Default = > < >`	[st_app1]
`Def term_eq(a;b) == Case(a) Case x;y = > Case(b) Case x';y' = > term_eq(x;x')term_eq(y;y') Case tree_leaf(x) = > false Default = > True Case tree_leaf(x) = > Case(b) Case x';y' = > false Case tree_leaf(x') = > (x=x') Default = > True Default = > True (recursive)`	[term_eq]