(3steps) PrintForm Definitions mb declaration Sections GenAutomata Doc

At: rename decl subtype 1 1
1. d: Decl
2. f: LabelLabel
3. x: Label
4. z: y:Label. if f(x) = f(y) d(y) else Top fi
5. z if f(x) = f(x) d(x) else Top fi

z d(x)
By:
EqLblReflexive -1
THEN
Trivial
Generated subgoals:

None

About:
ifthenelseisectapplyfunctionmembertop

(3steps) PrintForm Definitions mb declaration Sections GenAutomata Doc