Platform claims not to support CPU time, falling back to wall time. Cannot find out cpu time on external processes, falling back to wall time! Running Thread.stop() against 1423978004Exec. 6, RelTRSEmission[] Stack trace: aprove.DPFramework.BasicStructures.FunctionApplication.processSubstitution(FunctionApplication.java:260) aprove.DPFramework.BasicStructures.FunctionApplication.applySubstitution(FunctionApplication.java:255) aprove.DPFramework.BasicStructures.FunctionApplication.applySubstitution(FunctionApplication.java:26) aprove.DPFramework.BasicStructures.Term.rewrite(Term.java:1159) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:117) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:119) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.findEmittingSequence(RelTRSEmissionProcessor.java:87) aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.processRelTRS(RelTRSEmissionProcessor.java:135) aprove.DPFramework.TRSProblem.Processors.RelTRSProcessor.process(RelTRSProcessor.java:38) aprove.Strategies.ExecutableStrategies.Executor.execute(Executor.java:326) aprove.Strategies.ExecutableStrategies.Executor$Runner.wrappedRun(Executor.java:377) aprove.Strategies.Abortions.PooledJob.run(PooledJob.java:98) aprove.Strategies.Util.PrioritizableThreadPool$Worker.run(PrioritizableThreadPool.java:273) java.lang.Thread.run(Thread.java:744) Aborted 1423978004Exec. 6, RelTRSEmission[] with a hard timeout. Threadpool thread died by not catching an exception java.lang.ThreadDeath at aprove.Strategies.Abortions.PooledJob.finish(PooledJob.java:156) at aprove.Strategies.Abortions.PooledJob.run(PooledJob.java:124) at aprove.Strategies.Util.PrioritizableThreadPool$Worker.run(PrioritizableThreadPool.java:273) at java.lang.Thread.run(Thread.java:744) proof of /home/fs5/ayamada/tpdb/relative/Mixed_relative_TRS/rt-rw4.trs # AProVE Commit ID: 2b684c7cda508b1711f707cb42f127e64fe1df88 ffrohn 20140415 dirty Termination of the given RelTRS could be proven: (0) RelTRS (1) RelTRSRRRProof [EQUIVALENT, 674 ms] (2) RelTRS (3) RelTRSRRRProof [EQUIVALENT, 464 ms] (4) RelTRS (5) RelTRSRRRProof [EQUIVALENT, 648 ms] (6) RelTRS (7) RelTRSRRRProof [EQUIVALENT, 806 ms] (8) RelTRS (9) RelTRSRRRProof [EQUIVALENT, 2395 ms] (10) RelTRS (11) RelTRSRRRProof [EQUIVALENT, 716 ms] (12) RelTRS (13) RelTRSRRRProof [EQUIVALENT, 477 ms] (14) RelTRS (15) RelTRSRRRProof [EQUIVALENT, 616 ms] (16) RelTRS (17) RIsEmptyProof [EQUIVALENT, 1 ms] (18) YES ---------------------------------------- (0) Obligation: Relative term rewrite system: The relative TRS consists of the following R rules: RAo(R) -> R RAn(R) -> R WAo(W) -> W WAn(W) -> W The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) top(ok(sys_r(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_r(read(RAo(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_w(read(RAo(r), x), write(W, Ww)))) top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_r(read(RAn(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_w(read(RAn(r), x), write(W, Ww)))) top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_r(read(R, Rw), write(WAn(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_w(read(R, Rw), write(WAn(W), y)))) top(ok(sys_r(read(R, Rw), write(W, WIo(y))))) -> top(check(sys_r(read(R, Rw), write(WAo(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIo(y))))) -> top(check(sys_w(read(R, Rw), write(WAo(W), y)))) top(ok(sys_r(read(r, RIo(x)), write(W, y)))) -> top(check(sys_w(read(RAo(r), x), write(W, y)))) top(ok(sys_r(read(r, RIn(x)), write(W, y)))) -> top(check(sys_w(read(RAn(r), x), write(W, y)))) top(ok(sys_w(read(R, x), write(W, WIo(y))))) -> top(check(sys_r(read(R, x), write(WAo(W), y)))) top(ok(sys_w(read(R, x), write(W, WIn(y))))) -> top(check(sys_r(read(R, x), write(WAn(W), y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (1) RelTRSRRRProof (EQUIVALENT) We used the following monotonic ordering for rule removal: Polynomial interpretation [POLO]: POL(R) = 0 POL(RAn(x_1)) = x_1 POL(RAo(x_1)) = x_1 POL(RIn(x_1)) = x_1 POL(RIo(x_1)) = x_1 POL(Rw) = 0 POL(W) = 0 POL(WAn(x_1)) = x_1 POL(WAo(x_1)) = x_1 POL(WIn(x_1)) = x_1 POL(WIo(x_1)) = 1 + x_1 POL(Ww) = 0 POL(check(x_1)) = x_1 POL(ok(x_1)) = x_1 POL(read(x_1, x_2)) = x_1 + x_2 POL(sys_r(x_1, x_2)) = x_1 + x_2 POL(sys_w(x_1, x_2)) = x_1 + x_2 POL(top(x_1)) = x_1 POL(write(x_1, x_2)) = x_1 + x_2 With this ordering the following rules can be removed [MATRO] because they are oriented strictly: Rules from R: none Rules from S: top(ok(sys_r(read(R, Rw), write(W, WIo(y))))) -> top(check(sys_r(read(R, Rw), write(WAo(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIo(y))))) -> top(check(sys_w(read(R, Rw), write(WAo(W), y)))) top(ok(sys_w(read(R, x), write(W, WIo(y))))) -> top(check(sys_r(read(R, x), write(WAo(W), y)))) ---------------------------------------- (2) Obligation: Relative term rewrite system: The relative TRS consists of the following R rules: RAo(R) -> R RAn(R) -> R WAo(W) -> W WAn(W) -> W The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) top(ok(sys_r(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_r(read(RAo(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_w(read(RAo(r), x), write(W, Ww)))) top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_r(read(RAn(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_w(read(RAn(r), x), write(W, Ww)))) top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_r(read(R, Rw), write(WAn(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_w(read(R, Rw), write(WAn(W), y)))) top(ok(sys_r(read(r, RIo(x)), write(W, y)))) -> top(check(sys_w(read(RAo(r), x), write(W, y)))) top(ok(sys_r(read(r, RIn(x)), write(W, y)))) -> top(check(sys_w(read(RAn(r), x), write(W, y)))) top(ok(sys_w(read(R, x), write(W, WIn(y))))) -> top(check(sys_r(read(R, x), write(WAn(W), y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (3) RelTRSRRRProof (EQUIVALENT) We used the following monotonic ordering for rule removal: Polynomial interpretation [POLO]: POL(R) = 0 POL(RAn(x_1)) = x_1 POL(RAo(x_1)) = 1 + x_1 POL(RIn(x_1)) = x_1 POL(RIo(x_1)) = 1 + x_1 POL(Rw) = 0 POL(W) = 0 POL(WAn(x_1)) = x_1 POL(WAo(x_1)) = x_1 POL(WIn(x_1)) = x_1 POL(WIo(x_1)) = x_1 POL(Ww) = 0 POL(check(x_1)) = x_1 POL(ok(x_1)) = x_1 POL(read(x_1, x_2)) = x_1 + x_2 POL(sys_r(x_1, x_2)) = 1 + x_1 + x_2 POL(sys_w(x_1, x_2)) = 1 + x_1 + x_2 POL(top(x_1)) = x_1 POL(write(x_1, x_2)) = x_1 + x_2 With this ordering the following rules can be removed [MATRO] because they are oriented strictly: Rules from R: RAo(R) -> R Rules from S: none ---------------------------------------- (4) Obligation: Relative term rewrite system: The relative TRS consists of the following R rules: RAn(R) -> R WAo(W) -> W WAn(W) -> W The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) top(ok(sys_r(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_r(read(RAo(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_w(read(RAo(r), x), write(W, Ww)))) top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_r(read(RAn(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_w(read(RAn(r), x), write(W, Ww)))) top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_r(read(R, Rw), write(WAn(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_w(read(R, Rw), write(WAn(W), y)))) top(ok(sys_r(read(r, RIo(x)), write(W, y)))) -> top(check(sys_w(read(RAo(r), x), write(W, y)))) top(ok(sys_r(read(r, RIn(x)), write(W, y)))) -> top(check(sys_w(read(RAn(r), x), write(W, y)))) top(ok(sys_w(read(R, x), write(W, WIn(y))))) -> top(check(sys_r(read(R, x), write(WAn(W), y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (5) RelTRSRRRProof (EQUIVALENT) We used the following monotonic ordering for rule removal: Polynomial interpretation [POLO]: POL(R) = 0 POL(RAn(x_1)) = x_1 POL(RAo(x_1)) = 1 + x_1 POL(RIn(x_1)) = x_1 POL(RIo(x_1)) = 1 + x_1 POL(Rw) = 0 POL(W) = 0 POL(WAn(x_1)) = x_1 POL(WAo(x_1)) = 1 + x_1 POL(WIn(x_1)) = x_1 POL(WIo(x_1)) = x_1 POL(Ww) = 0 POL(check(x_1)) = x_1 POL(ok(x_1)) = x_1 POL(read(x_1, x_2)) = x_1 + x_2 POL(sys_r(x_1, x_2)) = 1 + x_1 + x_2 POL(sys_w(x_1, x_2)) = 1 + x_1 + x_2 POL(top(x_1)) = x_1 POL(write(x_1, x_2)) = x_1 + x_2 With this ordering the following rules can be removed [MATRO] because they are oriented strictly: Rules from R: WAo(W) -> W Rules from S: none ---------------------------------------- (6) Obligation: Relative term rewrite system: The relative TRS consists of the following R rules: RAn(R) -> R WAn(W) -> W The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) top(ok(sys_r(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_r(read(RAo(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_w(read(RAo(r), x), write(W, Ww)))) top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_r(read(RAn(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_w(read(RAn(r), x), write(W, Ww)))) top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_r(read(R, Rw), write(WAn(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_w(read(R, Rw), write(WAn(W), y)))) top(ok(sys_r(read(r, RIo(x)), write(W, y)))) -> top(check(sys_w(read(RAo(r), x), write(W, y)))) top(ok(sys_r(read(r, RIn(x)), write(W, y)))) -> top(check(sys_w(read(RAn(r), x), write(W, y)))) top(ok(sys_w(read(R, x), write(W, WIn(y))))) -> top(check(sys_r(read(R, x), write(WAn(W), y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (7) RelTRSRRRProof (EQUIVALENT) We used the following monotonic ordering for rule removal: Polynomial interpretation [POLO]: POL(R) = 0 POL(RAn(x_1)) = x_1 POL(RAo(x_1)) = x_1 POL(RIn(x_1)) = x_1 POL(RIo(x_1)) = 1 + x_1 POL(Rw) = 0 POL(W) = 0 POL(WAn(x_1)) = x_1 POL(WAo(x_1)) = x_1 POL(WIn(x_1)) = x_1 POL(WIo(x_1)) = x_1 POL(Ww) = 0 POL(check(x_1)) = x_1 POL(ok(x_1)) = x_1 POL(read(x_1, x_2)) = x_1 + x_2 POL(sys_r(x_1, x_2)) = x_1 + x_2 POL(sys_w(x_1, x_2)) = x_1 + x_2 POL(top(x_1)) = x_1 POL(write(x_1, x_2)) = x_1 + x_2 With this ordering the following rules can be removed [MATRO] because they are oriented strictly: Rules from R: none Rules from S: top(ok(sys_r(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_r(read(RAo(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIo(x)), write(W, Ww)))) -> top(check(sys_w(read(RAo(r), x), write(W, Ww)))) top(ok(sys_r(read(r, RIo(x)), write(W, y)))) -> top(check(sys_w(read(RAo(r), x), write(W, y)))) ---------------------------------------- (8) Obligation: Relative term rewrite system: The relative TRS consists of the following R rules: RAn(R) -> R WAn(W) -> W The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_r(read(RAn(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_w(read(RAn(r), x), write(W, Ww)))) top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_r(read(R, Rw), write(WAn(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_w(read(R, Rw), write(WAn(W), y)))) top(ok(sys_r(read(r, RIn(x)), write(W, y)))) -> top(check(sys_w(read(RAn(r), x), write(W, y)))) top(ok(sys_w(read(R, x), write(W, WIn(y))))) -> top(check(sys_r(read(R, x), write(WAn(W), y)))) check(RIo(x)) -> ok(RIo(x)) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIo(x)) -> RIo(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (9) RelTRSRRRProof (EQUIVALENT) We used the following monotonic ordering for rule removal: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) : <<< POL(RAn(x_1)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 >>> <<< POL(R) = [[0], [0]] >>> <<< POL(WAn(x_1)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 >>> <<< POL(W) = [[0], [0]] >>> <<< POL(Rw) = [[0], [0]] >>> <<< POL(RIn(x_1)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 >>> <<< POL(Ww) = [[0], [0]] >>> <<< POL(WIn(x_1)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 >>> <<< POL(top(x_1)) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< POL(ok(x_1)) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< POL(sys_r(x_1, x_2)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 + [[1, 0], [0, 1]] * x_2 >>> <<< POL(read(x_1, x_2)) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 + [[1, 0], [0, 0]] * x_2 >>> <<< POL(write(x_1, x_2)) = [[0], [0]] + [[1, 1], [1, 1]] * x_1 + [[1, 0], [0, 0]] * x_2 >>> <<< POL(check(x_1)) = [[0], [0]] + [[1, 1], [0, 1]] * x_1 >>> <<< POL(sys_w(x_1, x_2)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 + [[1, 0], [0, 1]] * x_2 >>> <<< POL(RIo(x_1)) = [[1], [1]] + [[1, 1], [0, 1]] * x_1 >>> <<< POL(RAo(x_1)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 >>> <<< POL(WAo(x_1)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 >>> <<< POL(WIo(x_1)) = [[0], [0]] + [[1, 0], [0, 1]] * x_1 >>> With this ordering the following rules can be removed [MATRO] because they are oriented strictly: Rules from R: none Rules from S: check(RIo(x)) -> ok(RIo(x)) check(RIo(x)) -> RIo(check(x)) ---------------------------------------- (10) Obligation: Relative term rewrite system: The relative TRS consists of the following R rules: RAn(R) -> R WAn(W) -> W The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_r(read(RAn(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_w(read(RAn(r), x), write(W, Ww)))) top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_r(read(R, Rw), write(WAn(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_w(read(R, Rw), write(WAn(W), y)))) top(ok(sys_r(read(r, RIn(x)), write(W, y)))) -> top(check(sys_w(read(RAn(r), x), write(W, y)))) top(ok(sys_w(read(R, x), write(W, WIn(y))))) -> top(check(sys_r(read(R, x), write(WAn(W), y)))) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (11) RelTRSRRRProof (EQUIVALENT) We used the following monotonic ordering for rule removal: Polynomial interpretation [POLO]: POL(R) = 0 POL(RAn(x_1)) = x_1 POL(RAo(x_1)) = x_1 POL(RIn(x_1)) = x_1 POL(Rw) = 0 POL(W) = 0 POL(WAn(x_1)) = x_1 POL(WAo(x_1)) = x_1 POL(WIn(x_1)) = x_1 POL(WIo(x_1)) = x_1 POL(Ww) = 0 POL(check(x_1)) = x_1 POL(ok(x_1)) = 1 + x_1 POL(read(x_1, x_2)) = x_1 + x_2 POL(sys_r(x_1, x_2)) = x_1 + x_2 POL(sys_w(x_1, x_2)) = x_1 + x_2 POL(top(x_1)) = x_1 POL(write(x_1, x_2)) = x_1 + x_2 With this ordering the following rules can be removed [MATRO] because they are oriented strictly: Rules from R: none Rules from S: top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_r(read(RAn(r), x), write(W, Ww)))) top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) -> top(check(sys_w(read(RAn(r), x), write(W, Ww)))) top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_r(read(R, Rw), write(WAn(W), y)))) top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) -> top(check(sys_w(read(R, Rw), write(WAn(W), y)))) top(ok(sys_r(read(r, RIn(x)), write(W, y)))) -> top(check(sys_w(read(RAn(r), x), write(W, y)))) top(ok(sys_w(read(R, x), write(W, WIn(y))))) -> top(check(sys_r(read(R, x), write(WAn(W), y)))) ---------------------------------------- (12) Obligation: Relative term rewrite system: The relative TRS consists of the following R rules: RAn(R) -> R WAn(W) -> W The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (13) RelTRSRRRProof (EQUIVALENT) We used the following monotonic ordering for rule removal: Polynomial interpretation [POLO]: POL(R) = 0 POL(RAn(x_1)) = 1 + x_1 POL(RAo(x_1)) = x_1 POL(RIn(x_1)) = x_1 POL(Rw) = 0 POL(W) = 0 POL(WAn(x_1)) = x_1 POL(WAo(x_1)) = x_1 POL(WIn(x_1)) = x_1 POL(WIo(x_1)) = x_1 POL(Ww) = 0 POL(check(x_1)) = x_1 POL(ok(x_1)) = x_1 POL(sys_r(x_1, x_2)) = x_1 + x_2 POL(sys_w(x_1, x_2)) = x_1 + x_2 With this ordering the following rules can be removed [MATRO] because they are oriented strictly: Rules from R: RAn(R) -> R Rules from S: none ---------------------------------------- (14) Obligation: Relative term rewrite system: The relative TRS consists of the following R rules: WAn(W) -> W The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (15) RelTRSRRRProof (EQUIVALENT) We used the following monotonic ordering for rule removal: Polynomial interpretation [POLO]: POL(RAn(x_1)) = x_1 POL(RAo(x_1)) = x_1 POL(RIn(x_1)) = x_1 POL(Rw) = 0 POL(W) = 0 POL(WAn(x_1)) = 1 + x_1 POL(WAo(x_1)) = x_1 POL(WIn(x_1)) = x_1 POL(WIo(x_1)) = x_1 POL(Ww) = 0 POL(check(x_1)) = x_1 POL(ok(x_1)) = x_1 POL(sys_r(x_1, x_2)) = x_1 + x_2 POL(sys_w(x_1, x_2)) = x_1 + x_2 With this ordering the following rules can be removed [MATRO] because they are oriented strictly: Rules from R: WAn(W) -> W Rules from S: none ---------------------------------------- (16) Obligation: Relative term rewrite system: R is empty. The relative TRS consists of the following S rules: Rw -> RIn(Rw) Ww -> WIn(Ww) check(RAo(x)) -> RAo(check(x)) check(RAn(x)) -> RAn(check(x)) check(WAo(x)) -> WAo(check(x)) check(WAn(x)) -> WAn(check(x)) check(RIn(x)) -> RIn(check(x)) check(WIo(x)) -> WIo(check(x)) check(WIn(x)) -> WIn(check(x)) check(sys_r(x, y)) -> sys_r(check(x), y) check(sys_r(x, y)) -> sys_r(x, check(y)) check(sys_w(x, y)) -> sys_w(check(x), y) check(sys_w(x, y)) -> sys_w(x, check(y)) RAo(ok(x)) -> ok(RAo(x)) RAn(ok(x)) -> ok(RAn(x)) WAo(ok(x)) -> ok(WAo(x)) WAn(ok(x)) -> ok(WAn(x)) RIn(ok(x)) -> ok(RIn(x)) WIo(ok(x)) -> ok(WIo(x)) WIn(ok(x)) -> ok(WIn(x)) sys_r(ok(x), y) -> ok(sys_r(x, y)) sys_r(x, ok(y)) -> ok(sys_r(x, y)) sys_w(ok(x), y) -> ok(sys_w(x, y)) sys_w(x, ok(y)) -> ok(sys_w(x, y)) ---------------------------------------- (17) RIsEmptyProof (EQUIVALENT) The TRS R is empty. Hence, termination is trivially proven. ---------------------------------------- (18) YES