Nuprl - mb_automata_1 Citations of ts

Def (a=b) == ts_case(a) var(v)= > ts_case(b) var(v')= > v =

v' var'(x)= > false

opr(x)= > false

fvar(x)= > false

trace(x)= > false

end_ts_case var'(p)= > ts_case(b) var(x)= > false

var'(p')= > p =

p' opr(x)= > false

fvar(x)= > false

trace(x)= > false

end_ts_case opr(op)= > ts_case(b) var(x)= > false

var'(x)= > false

opr(op')= > op =

op' fvar(x)= > false

trace(x)= > false

end_ts_case fvar(f)= > ts_case(b) var(x)= > false

var'(x)= > false

opr(x)= > false

fvar(f')= > f =

f' trace(x)= > false

end_ts_case trace(P)= > ts_case(b) var(x)= > false

var'(x)= > false

opr(x)= > false

fvar(x)= > false

trace(P')= > P =

P' end_ts_case end_ts_case

is mentioned by

Thm* a,b:ts(). (a=b) a = b [assert_ts_eq]

Try larger context: GenAutomata