0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 102 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 28 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 20 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → U1_GG(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
PB_IN_GGGG(T21, T23, T7, T22) → MEMBERC_IN_GG(T21, T23)
MEMBERC_IN_GG(T42, .(T43, T44)) → U3_GG(T42, T43, T44, memberC_in_gg(T42, T44))
MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_GGGG(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → U2_GG(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))
subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → U1_GG(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
PB_IN_GGGG(T21, T23, T7, T22) → MEMBERC_IN_GG(T21, T23)
MEMBERC_IN_GG(T42, .(T43, T44)) → U3_GG(T42, T43, T44, memberC_in_gg(T42, T44))
MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_GGGG(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → U2_GG(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))
subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))
MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)
subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))
MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)
MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)
From the DPs we obtained the following set of size-change graphs:
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))
subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
memberC_in_gg(x0, x1)
U3_gg(x0, x1, x2, x3)
From the DPs we obtained the following set of size-change graphs: