dim-test.egg

(sort Dim)
(function Dim_lit (i64) Dim)
(function Dim_var (String) Dim)
(function Dim___add__ (Dim Dim) Dim)
(function Dim___mul__ (Dim Dim) Dim)
(function dim_edge (Dim Dim) String :merge new)

(rule ((= tobematched_______0 (Dim___add__ (Dim_lit 0) a))
    (!= a (Dim_lit i1)))
  ((set (dim_edge (Dim___add__ (Dim_lit 0) a) a) "simpl#add_0_l"))
)
(rule ((= tobematched_______0 (Dim___add__ (Dim_lit i1) (Dim_lit i2)))
    (!= tobematched_______1 (Dim___mul__ tobematched_______0 x)))
  ((set (dim_edge (Dim___add__ (Dim_lit i1) (Dim_lit i2)) (Dim_lit (+ i1 i2))) "simpl#c-fold"))
)

(sort DimProof)
(function DimProof_refl (Dim) DimProof)
(function DimProof_trans (DimProof Dim String) DimProof)
(function DimProof_join (Dim DimProof DimProof) DimProof)
(function dim_path (Dim Dim) DimProof :unextractable)

(rule ((= s (dim_edge x y)))
  ((set (dim_path x y) (DimProof_trans (DimProof_refl y) x s)))
)
(rule ((= s (dim_edge x y))
    (= p (dim_path y z)))
  ((set (dim_path x z) (DimProof_trans p x s)))
)


(rule ((= a (Dim___add__ x1 x2))
    (= p1 (dim_path x1 y1))
    (= p2 (dim_path x2 y2)))
  ((set (dim_path a (Dim___add__ y1 y2)) (DimProof_join a p1 p2)))
)
(rule ((= a (Dim___add__ x1 x2))
    (= p1 (dim_path x1 y1)))
  ((set (dim_path a (Dim___add__ y1 x2)) (DimProof_join a p1 (DimProof_refl x2))))
)
(rule ((= a (Dim___add__ x1 x2))
    (= p2 (dim_path x2 y2)))
  ((set (dim_path a (Dim___add__ x1 y2)) (DimProof_join a (DimProof_refl x1) p2)))
)


(let ___________int_const__0 (Dim_lit 0))
(let ___________int_const__1 (Dim_lit 1))
(let ___________int_const__2 (Dim_lit 2))
(let ___________int_const__3 (Dim_lit 2))
(let x (Dim_var "x"))
(let lhsdim (Dim___add__ (Dim___add__ ___________int_const__2 ___________int_const__1) (Dim___add__ ___________int_const__0 x)))
(let rhsdim (Dim___add__ ___________int_const__3 x))

(relation dim_goals (Dim Dim))
(dim_goals lhsdim rhsdim)

(run 100)
(print-function dim_goals 100)
(print-function dim_edge 100)
(print-function dim_path 100)
(extract (dim_path lhsdim rhsdim))