{{{ A rough set of examples (using the refined 'chr-based' algorithm) Assuming a normal form of equations, it is sufficient to apply the following 'FD'-rule step. e1: F t1 = t2 e2: F t1 = t3 ==> e1: F t1 = t2 e2: F t1 = t3 e3: t2 = t3 where e3 = (sym e1) trans e2 Here are some examples: EXAMPLE 1 Assume (given) g : forall a. S [a] = [S a] -- axiom d1 : T Int = Int -- local equations d2 : T [Int] = S [Int] d3 : T Int = S Int wanted ? : T [Int] = [Int] Step 1: Normalize (local and wanted) equations (also applies to axioms but we skip this step here) g : forall a. S [a] = [S a] (0) g1 : T Int = Int (1) g2 : T [Int] = a (2) g3 : S [Int] = a (3) g4 : T Int = b (4) g5 : S Int = b (5) ? : T [Int] = [Int] (6) Reduction steps: 2+6 => ?' : a = [Int] ? = g2 trans ?' 03 from 0+3 => g03 : a = [S Int] g03 = (sym g3) trans (g Int) 503 from 5+03 => g503 : a = [b] g503 = g03 trans ([] g5) 14 from 1+4 => g14 : b = Int g14 = (sym g4) trans g1 Apply 14 on 503 => g' : a = [Int] g' = g503 trans ([] g14) We found a match for the (reduced) wanted constraint. ? = g2 trans ?' = g2 trans (g503 trans ([] g14)) = g2 trans ((g03 trans ([] g5)) trans ([] g14)) = g2 trans ((((sym g3) trans (g Int)) trans ([] g5)) trans ([] g14)) How to map back to the original (given) local equations? The same calculation using the original (given) local equations. g : forall a. S [a] = [S a] (0) -- axiom d1 : T Int = Int (1) -- local equations d2 : T [Int] = S [Int] (2) d3 : T Int = S Int (3) wanted: d4 : T [Int] = [Int] (4) Reduction steps: 24: 2+4 => d24 : S [Int] = [Int] d4 = d2 trans d24 -- wanted, we're interested how to construct d4! 024: 0+24 => d024 : [S Int] = [Int] d24 = (sym (g Int)) trans d024 deompose => d024' : S Int = Int d024 = [] d024' 13 : 1+3 => d13 : S Int = Int d13 = (sym d3) trans d1 We found a match for the (reduced) wanted constraint. d024' = d13 = (sym d3) trans d1 Thus, d4 = d2 trans d24 = d2 trans ((sym (g Int)) trans d024) = d2 trans ((sym (g Int)) trans ([] d024')) = d2 trans ((sym (g Int)) trans ([] ((sym d3) trans d1))) Compare the normalized result g2 trans ((((sym g3) trans (g Int)) trans ([] g5)) trans ([] g14)) against the 'unnormalized' result d2 trans ((sym (g Int)) trans ([] ((sym d3) trans d1))) EXAMPLE 2 no axioms involved given: d1 : G Int = Bool d2 : F (G Int) = Int wanted: d : F Bool = Int clearly d = (sym (F d1)) trans d2 The normalized case: g1 : G Int = Bool (1) g2 : G Int = a (2) g3 : F a = Int (3) Reductions: 12 from 1 + 2 => g12 : a = Bool g12 = (sym g2) trans g1 apply 12 on g3: g3' : F Bool = Int g3' = (sym (F g12)) trans g3 Match found, we find d = (sym (F g12)) trans g3 = (sym (F ((sym g2) trans g1))) trans g3 compare with (sym (F d1)) trans d2 }}}