Nuprl - mb automata 2 Citations of term eq

mb automata 2 Sections GenAutomata Doc

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)

is mentioned by

Thm* a,b:Term. term_eq(a;b) a = b [assert_term_eq]

Def termlist_eq(a;b) == Case of a; nil Case of b; nil true ; x.xs false ; x.xs Case of b; nil false ; x'.xs' term_eq(x;x')termlist_eq(xs;xs') (recursive) [termlist_eq]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc

`Thm* a,b:Term. term_eq(a;b) a = b`	[assert_term_eq]
`Def termlist_eq(a;b) == Case of a; nil Case of b; nil true ; x.xs false ; x.xs Case of b; nil false ; x'.xs' term_eq(x;x')termlist_eq(xs;xs') (recursive)`	[termlist_eq]