AProVE Web Interface

This is the AProVE Web Interface for the current version of AProVE.

Analysis of (Probabilistic) Term Rewrite System (new ARI Format)

Show Help for the new ARI input format (in new window). See also here for the new ARI format of probabilistic TRSs.

(format PTRS)

(GOAL AST)

(STRATEGY INNERMOST)

(fun rotate 1)
(fun cons 2)
(fun app 2)
(fun nil 0)
(fun leq 2)
(fun 0 0)
(fun true 0)
(fun low 2)
(fun ifLow 3)
(fun high 2)
(fun s 1)
(fun false 0)
(fun qsHelp 1)
(fun qs 1)
(fun ifHigh 3)

(prule (rotate (cons x xs)) (((cons x xs) :prob 1 ) ((rotate (app (rotate xs) (cons x nil))) :prob 1 )))
(prule (leq 0 x) ((true :prob 1 )))
(prule (low x nil) ((nil :prob 1 )))
(prule (ifLow true x (cons y ys)) (((low x ys) :prob 1 )))
(prule (high x nil) ((nil :prob 1 )))
(prule (leq (s x) 0) ((false :prob 1 )))
(prule (app nil ys) ((ys :prob 1 )))
(prule (app (cons x xs) ys) (((cons x (app xs ys)) :prob 1 )))
(prule (rotate nil) ((nil :prob 1 )))
(prule (qsHelp (cons x xs)) (((app (qs (low x xs)) (cons x (qs (high x xs)))) :prob 1 )))
(prule (low x (cons y ys)) (((ifLow (leq x y) x (cons y ys)) :prob 1 )))
(prule (leq (s x) (s y)) (((leq x y) :prob 1 )))
(prule (qs nil) ((nil :prob 1 )))
(prule (qs (cons x xs)) (((qsHelp (rotate (cons x xs))) :prob 1 )))
(prule (high x (cons y ys)) (((ifHigh (leq x y) x (cons y ys)) :prob 1 )))
(prule (ifLow false x (cons y ys)) (((cons y (low x ys)) :prob 1 )))
(prule (ifHigh false x (cons y ys)) (((high x ys) :prob 1 )))
(prule (ifHigh true x (cons y ys)) (((cons y (high x ys)) :prob 1 )))

Choose file

Accepted file formats: ari

Upload a File or Text?

Timeout (1 seconds minimum, 300 seconds maximum):

Output format:

HTML

Plain Text

Version AProVE2023