; proofs of connectivity are paths
(datatype Proof
  (Trans i64 Proof)
  (Edge i64 i64))

; We enhance the path relation to carry a proof field
(relation path (i64 i64 Proof))
(relation edge (i64 i64))

(edge 2 1)
(edge 3 2)
(edge 1 3)

(rule ((edge x y))  
      ((path x y (Edge x y))))
(rule ((edge x y) (path y z p))  
      ((path x z (Trans x p))))

; We consider equal all paths tha connect same points.
; Smallest Extraction will extract shortest path.
(rule ((path x y p1) (path x y p2))  
      ((union p1 p2)))

(run 3)
(check (path 3 1 (Trans 3 (Edge 2 1))))
; Would prefer being able to check
;(check (path 1 2 _))
; or extract
;(query-extract (path 1 4 ?p))
(print-function path 100)