0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 QDPOrderProof (⇔)
↳27 QDP
↳28 PisEmptyProof (⇔)
↳29 TRUE
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
MSORT(.(x, y)) → MIN(x, y)
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
MSORT(.(x, y)) → DEL(min(x, y), .(x, y))
MIN(x, .(y, z)) → MIN(x, z)
MIN(x, .(y, z)) → MIN(y, z)
DEL(x, .(y, z)) → DEL(x, z)
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
DEL(x, .(y, z)) → DEL(x, z)
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
DEL(x, .(y, z)) → DEL(x, z)
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
DEL(x, .(y, z)) → DEL(x, z)
From the DPs we obtained the following set of size-change graphs:
MIN(x, .(y, z)) → MIN(y, z)
MIN(x, .(y, z)) → MIN(x, z)
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
MIN(x, .(y, z)) → MIN(y, z)
MIN(x, .(y, z)) → MIN(x, z)
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
MIN(x, .(y, z)) → MIN(y, z)
MIN(x, .(y, z)) → MIN(x, z)
From the DPs we obtained the following set of size-change graphs:
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
del(x, nil) → nil
msort(nil)
msort(.(x0, x1))
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
msort(nil)
msort(.(x0, x1))
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
del(x, nil) → nil
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
POL(.(x1, x2)) = 1 + x1 + x2
POL(<=(x1, x2)) = 0
POL(=(x1, x2)) = 0
POL(MSORT(x1)) = x1
POL(del(x1, x2)) = 0
POL(if(x1, x2, x3)) = 0
POL(min(x1, x2)) = 1 + x1
POL(nil) = 0
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
del(x, nil) → nil
min(x0, nil)
min(x0, .(x1, x2))
del(x0, nil)
del(x0, .(x1, x2))