Step-by-step reduction of ITerm expressions to normal form. Rules from ISAR.IStep · confluence from ISAR.IRed_confluence · unique normal forms from ISAR.isar_fragment_unique_normal_forms.
| Name | Pattern | Result |
|---|---|---|
| norm-elim | norm · x | x |
| konst-elim | konst · x · y | x |
| comp-elim | comp · f · g · x | f · (g · x) |
| dup-elim | dup · f · x | f · x · x |
| swap-elim | swap · f · x · y | f · y · x |
| ss-elim | ss · x · y · z | (x · z) · (y · z) |