c,a,b:
. a+b = c 
((a+b) ~ c)a,b,a',b':
. b-a = b'-a' ({a..b
} ~ {a'..b'})a,b:, c:{a...b}. ({a..c}+{c..b}) ~ {a..b}| Rank | Theorem | Name |
| 5 | c,a,b:. a+b = c ((a+b) ~ c) | [nsub_add] |
| cites the following: | ||
| 0 | a,b,a',b':. b-a = b'-a' ({a..b} ~ {a'..b'}) | [intseg_shift] |
| 4 | a,b:, c:{a...b}. ({a..c}+{c..b}) ~ {a..b} | [intseg_split] |