diff options
Diffstat (limited to 'src/equation.ts')
| -rw-r--r-- | src/equation.ts | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/equation.ts b/src/equation.ts index 0ec25d6..cc668b1 100644 --- a/src/equation.ts +++ b/src/equation.ts @@ -1,4 +1,4 @@ -import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem'; +import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr, SubstEq } from './utils/theorem'; export namespace equation { type F<X extends Op> = { op: 'F', a: X }; @@ -9,7 +9,6 @@ export namespace equation { export type Congruence<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<F<A>, F<B>>>; - export type SubstituteEq<O extends Equation<Op, Op>> = Rewrite<O['a'], O['b']> export interface SubstituteEq_Proof<A extends Op, B extends Op> { type: 'rewrite', known: { @@ -18,7 +17,7 @@ export namespace equation { left: Equation<F<A>, F<B>>; // f(a) = f(b) right: ChainRewrites<[ Sym<Congruence<A, B>>, // a = b - SubstituteEq<this['known']['a = b']>, // b = b + SubstEq<this['known']['a = b']>, // b = b Reflexivity<B>, ], this['left']>; }; @@ -36,8 +35,8 @@ export namespace equation { }, left: Equation<Equation<A, B>, Equation<B, C>>; // (a = b) = (b = c) right: ChainRewrites<[ - SubstituteEq<this['known']['a = b']>, // (b = b) = (b = c) - SubstituteEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>, // (b = b) = (c = b) + SubstEq<this['known']['a = b']>, // (b = b) = (b = c) + SubstEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>, // (b = b) = (c = b) Reflexivity<B>, // true = (b = b) Reflexivity<B>, // true = true Reflexivity<'true'>, |