1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
import { addition } from '../natural-numbers';
import { Add, _0 } from '../utils/nat';
import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem';
export type specChainRewrites = [
assert<Eq<
ChainRewrites<
[
addition.Commutativity<_0, 'B'>,
addition.Identity<'B'>,
],
Add<Add<_0, 'B'>, 'C'>
>,
Add<'B', 'C'>
>>,
assert<Eq<
ChainRewrites<
[
addition.Commutativity<_0, 'B'>,
addition.Identity<'B'>,
Sym<addition.Identity<Add<'B', 'C'>>>,
addition.Commutativity<Add<'B', 'C'>, _0>,
],
Add<Add<_0, 'B'>, 'C'>
>,
Add<_0, Add<'B', 'C'>>
>>,
]
|
