Jackie Shen

very very serious drawback: when we know p(p(1,2), 0) = 1, then if you ask p(1,2) = 1, kernel compares p(1,2) = p(p(1,2),0), then 1 = p(1,2) is checked again

1

**TODO:** There is a fundamental problem with the main loop in `cmpFc` and `fcEqualSpec`, which may lead to **circular reasoning**. For example, given $$ \text{know } p(p(1,2), 0) = 1,...

``` fn cx(a, b R) C fn cmul(a, b C) C know forall a, b, c, d R => cmul(cx(a, b), cx(c, d)) = cx(a*c-b*d, a*d+b*c) cx(0, 1) \cmul cx(0,...

fn compose(set1, set2, set3 nonempty_set, f fn(set2) set3, g fn(set1) set2) fn(set1) set3: forall x set1: compose(set1, set2, set3, f, g)(x) = f(g(x)) claim: @function_composition_associativity(S_1, S_2, S_3, S_4 nonempty_set, f...