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)
v'var'(x)= > falseopr(x)= > falsefvar(x)= > falsetrace(x)= > falseend_ts_case var'(p)= > ts_case(b)var(x)= > falsevar'(p')= > p = p'opr(x)= > falsefvar(x)= > falsetrace(x)= > falseend_ts_case opr(op)= > ts_case(b)var(x)= > falsevar'(x)= > falseopr(op')= > op = op'fvar(x)= > falsetrace(x)= > falseend_ts_case fvar(f)= > ts_case(b)var(x)= > falsevar'(x)= > falseopr(x)= > falsefvar(f')= > f = f'trace(x)= > falseend_ts_case trace(P)= > ts_case(b)var(x)= > falsevar'(x)= > falseopr(x)= > falsefvar(x)= > falsetrace(P')= > P = P'end_ts_case end_ts_case
is mentioned by
| 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 automata 1
Try larger context:
GenAutomata