R
↳Dependency Pair Analysis
EVENODD(x, 0) -> NOT(evenodd(x, s(0)))
EVENODD(x, 0) -> EVENODD(x, s(0))
EVENODD(s(x), s(0)) -> EVENODD(x, 0)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
EVENODD(s(x), s(0)) -> EVENODD(x, 0)
EVENODD(x, 0) -> EVENODD(x, s(0))
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(x, 0) -> EVENODD(x, s(0))
EVENODD(s(x''), 0) -> EVENODD(s(x''), s(0))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Forward Instantiation Transformation
EVENODD(s(x''), 0) -> EVENODD(s(x''), s(0))
EVENODD(s(x), s(0)) -> EVENODD(x, 0)
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(x), s(0)) -> EVENODD(x, 0)
EVENODD(s(s(x'''')), s(0)) -> EVENODD(s(x''''), 0)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 3
↳Forward Instantiation Transformation
EVENODD(s(s(x'''')), s(0)) -> EVENODD(s(x''''), 0)
EVENODD(s(x''), 0) -> EVENODD(s(x''), s(0))
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(x''), 0) -> EVENODD(s(x''), s(0))
EVENODD(s(s(x'''''')), 0) -> EVENODD(s(s(x'''''')), s(0))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 4
↳Forward Instantiation Transformation
EVENODD(s(s(x'''''')), 0) -> EVENODD(s(s(x'''''')), s(0))
EVENODD(s(s(x'''')), s(0)) -> EVENODD(s(x''''), 0)
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(s(x'''')), s(0)) -> EVENODD(s(x''''), 0)
EVENODD(s(s(s(x''''''''))), s(0)) -> EVENODD(s(s(x'''''''')), 0)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 5
↳Forward Instantiation Transformation
EVENODD(s(s(s(x''''''''))), s(0)) -> EVENODD(s(s(x'''''''')), 0)
EVENODD(s(s(x'''''')), 0) -> EVENODD(s(s(x'''''')), s(0))
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(s(x'''''')), 0) -> EVENODD(s(s(x'''''')), s(0))
EVENODD(s(s(s(x''''''''''))), 0) -> EVENODD(s(s(s(x''''''''''))), s(0))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 6
↳Forward Instantiation Transformation
EVENODD(s(s(s(x''''''''''))), 0) -> EVENODD(s(s(s(x''''''''''))), s(0))
EVENODD(s(s(s(x''''''''))), s(0)) -> EVENODD(s(s(x'''''''')), 0)
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(s(s(x''''''''))), s(0)) -> EVENODD(s(s(x'''''''')), 0)
EVENODD(s(s(s(s(x'''''''''''')))), s(0)) -> EVENODD(s(s(s(x''''''''''''))), 0)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 7
↳Forward Instantiation Transformation
EVENODD(s(s(s(s(x'''''''''''')))), s(0)) -> EVENODD(s(s(s(x''''''''''''))), 0)
EVENODD(s(s(s(x''''''''''))), 0) -> EVENODD(s(s(s(x''''''''''))), s(0))
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(s(s(x''''''''''))), 0) -> EVENODD(s(s(s(x''''''''''))), s(0))
EVENODD(s(s(s(s(x'''''''''''''')))), 0) -> EVENODD(s(s(s(s(x'''''''''''''')))), s(0))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 8
↳Forward Instantiation Transformation
EVENODD(s(s(s(s(x'''''''''''''')))), 0) -> EVENODD(s(s(s(s(x'''''''''''''')))), s(0))
EVENODD(s(s(s(s(x'''''''''''')))), s(0)) -> EVENODD(s(s(s(x''''''''''''))), 0)
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(s(s(s(x'''''''''''')))), s(0)) -> EVENODD(s(s(s(x''''''''''''))), 0)
EVENODD(s(s(s(s(s(x''''''''''''''''))))), s(0)) -> EVENODD(s(s(s(s(x'''''''''''''''')))), 0)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 9
↳Forward Instantiation Transformation
EVENODD(s(s(s(s(s(x''''''''''''''''))))), s(0)) -> EVENODD(s(s(s(s(x'''''''''''''''')))), 0)
EVENODD(s(s(s(s(x'''''''''''''')))), 0) -> EVENODD(s(s(s(s(x'''''''''''''')))), s(0))
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(s(s(s(x'''''''''''''')))), 0) -> EVENODD(s(s(s(s(x'''''''''''''')))), s(0))
EVENODD(s(s(s(s(s(x''''''''''''''''''))))), 0) -> EVENODD(s(s(s(s(s(x''''''''''''''''''))))), s(0))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 10
↳Forward Instantiation Transformation
EVENODD(s(s(s(s(s(x''''''''''''''''''))))), 0) -> EVENODD(s(s(s(s(s(x''''''''''''''''''))))), s(0))
EVENODD(s(s(s(s(s(x''''''''''''''''))))), s(0)) -> EVENODD(s(s(s(s(x'''''''''''''''')))), 0)
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)
one new Dependency Pair is created:
EVENODD(s(s(s(s(s(x''''''''''''''''))))), s(0)) -> EVENODD(s(s(s(s(x'''''''''''''''')))), 0)
EVENODD(s(s(s(s(s(s(x'''''''''''''''''''')))))), s(0)) -> EVENODD(s(s(s(s(s(x''''''''''''''''''''))))), 0)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 11
↳Remaining Obligation(s)
EVENODD(s(s(s(s(s(s(x'''''''''''''''''''')))))), s(0)) -> EVENODD(s(s(s(s(s(x''''''''''''''''''''))))), 0)
EVENODD(s(s(s(s(s(x''''''''''''''''''))))), 0) -> EVENODD(s(s(s(s(s(x''''''''''''''''''))))), s(0))
not(true) -> false
not(false) -> true
evenodd(x, 0) -> not(evenodd(x, s(0)))
evenodd(0, s(0)) -> false
evenodd(s(x), s(0)) -> evenodd(x, 0)