; @author Jonas Schöpf
; @author Fabian Mitterwallner
; @author Aart Middeldorp
; @doi 10.48550/arXiv.2402.13552
; Example 3 (specific instance where N = 1)
(format LCTRS :smtlib 2.6)

(theory Ints)

(sort PCP)
(sort String)

(fun e String)
(fun zero (-> String String))
(fun one (-> String String))
(fun start PCP)
(fun bot PCP)
(fun top PCP)
(fun test (-> String String Int PCP))
(fun alpha (-> Int String))
(fun beta (-> Int String))

(rule start (test (alpha n) (beta n) n) :guard (> n 0))
(rule (test e e n) top)
(rule (test (zero x) (zero y) n) (test x y n))
(rule (test (one x) (one y) n) (test x y n))
(rule (test (one x) (zero y) n) bot)
(rule (test (zero x) (one y) n) bot)
(rule (test (zero x) e n) bot)
(rule (test (one x) e n) bot)
(rule (test e (zero y) n) bot)
(rule (test e (one y) n) bot)
(rule (alpha 0) e)
(rule (beta 0) e)
(rule (alpha n) (one (zero (alpha m))) :guard (and (= (+ (* 1 m) 1) n) (> n 0)))
(rule (beta n) (zero (zero (beta m))) :guard (and (= (+ (* 1 m) 1) n) (> n 0)))