Problem: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(x,+(y,z)) Proof: Church Rosser Transformation Processor (critical pair closing system, Thm 2.4): strict: weak: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(x,+(y,z)) original problem: +(x110,0()) -> x110 +(x113,+(0(),x112)) -> +(+(x113,0()),x112) +(x134,s(x133)) -> s(+(x134,x133)) +(x137,+(x136,x135)) -> +(+(x137,x136),x135) +(+(x151,x150),x149) -> +(x151,+(x150,x149)) +(x160,+(s(x159),x158)) -> +(+(x160,s(x159)),x158) +(x201,+(x200,s(x199))) -> +(+(x201,x200),s(x199)) critical peaks: Shift Processor (no label): +(x110,0()) -> x110 +(x113,+(0(),x112)) -> +(+(x113,0()),x112) +(x134,s(x133)) -> s(+(x134,x133)) +(x137,+(x136,x135)) -> +(+(x137,x136),x135) +(+(x151,x150),x149) -> +(x151,+(x150,x149)) +(x160,+(s(x159),x158)) -> +(+(x160,s(x159)),x158) +(x201,+(x200,s(x199))) -> +(+(x201,x200),s(x199)) Church Rosser Transformation Processor (critical pair closing system, Thm 2.4): strict: weak: +(x110,0()) -> x110 +(x113,+(0(),x112)) -> +(+(x113,0()),x112) +(x134,s(x133)) -> s(+(x134,x133)) +(x137,+(x136,x135)) -> +(+(x137,x136),x135) +(+(x151,x150),x149) -> +(x151,+(x150,x149)) +(x160,+(s(x159),x158)) -> +(+(x160,s(x159)),x158) +(x201,+(x200,s(x199))) -> +(+(x201,x200),s(x199)) original problem: +(x649,0()) -> x649 +(x654,+(0(),x655)) -> +(+(x654,0()),x655) +(+(0(),0()),x661) -> +(0(),+(0(),x661)) +(+(x662,0()),x664) -> +(x662,+(0(),x664)) +(+(x667,x668),x670) -> +(x667,+(x668,x670)) +(x675,+(x676,x678)) -> +(+(x675,x676),x678) +(+(s(x685),0()),x686) -> +(s(x685),+(0(),x686)) +(+(x687,s(x688)),x690) -> +(x687,+(s(x688),x690)) +(x702,s(x704)) -> s(+(x702,x704)) +(x753,+(s(x754),x755)) -> +(+(x753,s(x754)),x755) +(+(0(),x812),x813) -> +(0(),+(x812,x813)) +(+(s(x844),x845),x846) -> +(s(x844),+(x845,x846)) +(x870,+(x871,s(x872))) -> +(+(x870,x871),s(x872)) +(+(x920,x921),s(x922)) -> +(x920,+(x921,s(x922))) +(+(0(),s(x931)),x932) -> +(0(),+(s(x931),x932)) +(+(s(x963),s(x964)),x965) -> +(s(x963),+(s(x964),x965)) +(+(0(),x971),s(x972)) -> +(0(),+(x971,s(x972))) +(+(s(x1003),x1004),s(x1005)) -> +(s(x1003),+(x1004,s(x1005))) critical peaks: Shift Processor (no label): +(x649,0()) -> x649 +(x654,+(0(),x655)) -> +(+(x654,0()),x655) +(+(0(),0()),x661) -> +(0(),+(0(),x661)) +(+(x662,0()),x664) -> +(x662,+(0(),x664)) +(+(x667,x668),x670) -> +(x667,+(x668,x670)) +(x675,+(x676,x678)) -> +(+(x675,x676),x678) +(+(s(x685),0()),x686) -> +(s(x685),+(0(),x686)) +(+(x687,s(x688)),x690) -> +(x687,+(s(x688),x690)) +(x702,s(x704)) -> s(+(x702,x704)) +(x753,+(s(x754),x755)) -> +(+(x753,s(x754)),x755) +(+(0(),x812),x813) -> +(0(),+(x812,x813)) +(+(s(x844),x845),x846) -> +(s(x844),+(x845,x846)) +(x870,+(x871,s(x872))) -> +(+(x870,x871),s(x872)) +(+(x920,x921),s(x922)) -> +(x920,+(x921,s(x922))) +(+(0(),s(x931)),x932) -> +(0(),+(s(x931),x932)) +(+(s(x963),s(x964)),x965) -> +(s(x963),+(s(x964),x965)) +(+(0(),x971),s(x972)) -> +(0(),+(x971,s(x972))) +(+(s(x1003),x1004),s(x1005)) -> +(s(x1003),+(x1004,s(x1005))) Church Rosser Transformation Processor: strict: weak: critical peaks: 340 +(x654,0()) <-0|1[]- +(x654,+(0(),0())) -1|[]-> +(+(x654,0()),0()) +(0(),0()) <-0|[]- +(+(0(),0()),0()) -2|[]-> +(0(),+(0(),0())) +(0(),x661) <-0|0[]- +(+(0(),0()),x661) -2|[]-> +(0(),+(0(),x661)) +(x662,0()) <-0|[]- +(+(x662,0()),0()) -3|[]-> +(x662,+(0(),0())) +(x662,x664) <-0|0[]- +(+(x662,0()),x664) -3|[]-> +(x662,+(0(),x664)) +(x667,x668) <-0|[]- +(+(x667,x668),0()) -4|[]-> +(x667,+(x668,0())) +(x667,x670) <-0|0[]- +(+(x667,0()),x670) -4|[]-> +(x667,+(0(),x670)) +(x675,x676) <-0|1[]- +(x675,+(x676,0())) -5|[]-> +(+(x675,x676),0()) +(s(x685),0()) <-0|[]- +(+(s(x685),0()),0()) -6|[]-> +(s(x685),+(0(),0())) +(s(x685),x686) <-0|0[]- +(+(s(x685),0()),x686) -6|[]-> +(s(x685),+(0(),x686)) +(x687,s(x688)) <-0|[]- +(+(x687,s(x688)),0()) -7|[]-> +(x687,+(s(x688),0())) +(x753,s(x754)) <-0|1[]- +(x753,+(s(x754),0())) -9|[]-> +(+(x753,s(x754)),0()) +(0(),x812) <-0|[]- +(+(0(),x812),0()) -10|[]-> +(0(),+(x812,0())) +(0(),x813) <-0|0[]- +(+(0(),0()),x813) -10|[]-> +(0(),+(0(),x813)) +(s(x844),x845) <-0|[]- +(+(s(x844),x845),0()) -11|[]-> +(s(x844),+(x845,0())) +(s(x844),x846) <-0|0[]- +(+(s(x844),0()),x846) -11|[]-> +(s(x844),+(0(),x846)) +(x920,s(x922)) <-0|0[]- +(+(x920,0()),s(x922)) -13|[]-> +(x920,+(0(),s(x922))) +(0(),s(x931)) <-0|[]- +(+(0(),s(x931)),0()) -14|[]-> +(0(),+(s(x931),0())) +(s(x963),s(x964)) <-0|[]- +(+(s(x963),s(x964)),0()) -15|[]-> +(s(x963),+(s(x964),0())) +(0(),s(x972)) <-0|0[]- +(+(0(),0()),s(x972)) -16|[]-> +(0(),+(0(),s(x972))) +(s(x1003),s(x1005)) <-0|0[]- +(+(s(x1003),0()),s(x1005)) -17| []-> +(s(x1003),+(0(),s(x1005))) +(x654,+(+(0(),0()),x3441)) <-1|1[]- +(x654,+(0(),+(0(),x3441))) -1| []-> +(+(x654,0()),+(0(),x3441)) +(+(+(0(),0()),0()),x3443) <-1|[]- +(+(0(),0()),+(0(),x3443)) -2| []-> +(0(),+(0(),+(0(),x3443))) +(+(+(x662,0()),0()),x3445) <-1|[]- +(+(x662,0()),+(0(),x3445)) -3| []-> +(x662,+(0(),+(0(),x3445))) +(+(+(x667,x668),0()),x3447) <-1|[]- +(+(x667,x668),+(0(),x3447)) -4| []-> +(x667,+(x668,+(0(),x3447))) +(+(+(x667,0()),x3449),x670) <-1|0[]- +(+(x667,+(0(),x3449)),x670) -4| []-> +(x667,+(+(0(),x3449),x670)) +(+(x675,0()),x678) <-1|[]- +(x675,+(0(),x678)) -5|[]-> +(+(x675,0()),x678) +(x675,+(+(x676,0()),x3453)) <-1|1[]- +(x675,+(x676,+(0(),x3453))) -5| []-> +(+(x675,x676),+(0(),x3453)) +(+(+(s(x685),0()),0()),x3455) <-1|[]- +(+(s(x685),0()),+(0(),x3455)) -6| []-> +(s(x685),+(0(),+(0(),x3455))) +(+(+(x687,s(x688)),0()),x3457) <-1|[]- +(+(x687,s(x688)),+(0(),x3457)) -7| []-> +(x687,+(s(x688),+(0(),x3457))) +(x753,+(+(s(x754),0()),x3459)) <-1|1[]- +(x753,+(s(x754),+(0(),x3459))) -9| []-> +(+(x753,s(x754)),+(0(),x3459)) +(+(+(0(),x812),0()),x3461) <-1|[]- +(+(0(),x812),+(0(),x3461)) -10| []-> +(0(),+(x812,+(0(),x3461))) +(+(+(0(),0()),x3463),x813) <-1|0[]- +(+(0(),+(0(),x3463)),x813) -10| []-> +(0(),+(+(0(),x3463),x813)) +(+(+(s(x844),x845),0()),x3465) <-1|[]- +(+(s(x844),x845),+(0(),x3465)) -11| []-> +(s(x844),+(x845,+(0(),x3465))) +(+(+(s(x844),0()),x3467),x846) <-1|0[]- +(+(s(x844),+(0(),x3467)),x846) -11| []-> +(s(x844),+(+(0(),x3467),x846)) +(+(x870,0()),s(x872)) <-1|[]- +(x870,+(0(),s(x872))) -12|[]-> +(+(x870,0()),s(x872)) +(+(+(x920,0()),x3471),s(x922)) <-1|0[]- +(+(x920,+(0(),x3471)),s(x922)) -13| []-> +(x920,+(+(0(),x3471),s(x922))) +(+(+(0(),s(x931)),0()),x3473) <-1|[]- +(+(0(),s(x931)),+(0(),x3473)) -14| []-> +(0(),+(s(x931),+(0(),x3473))) +(+(+(s(x963),s(x964)),0()),x3475) <-1|[]- +(+(s(x963),s(x964)),+(0(),x3475)) -15| []-> +(s(x963),+(s(x964),+(0(),x3475))) +(+(+(0(),0()),x3477),s(x972)) <-1|0[]- +(+(0(),+(0(),x3477)),s(x972)) -16| []-> +(0(),+(+(0(),x3477),s(x972))) +(+(+(s(x1003),0()),x3479),s(x1005)) <-1|0[]- +(+(s(x1003),+(0(),x3479)),s(x1005)) -17| []-> +(s(x1003),+(+(0(),x3479),s(x1005))) +(0(),+(0(),0())) <-2|[]- +(+(0(),0()),0()) -0|[]-> +(0(),0()) +(0(),+(0(),+(0(),x655))) <-2|[]- +(+(0(),0()),+(0(),x655)) -1| []-> +(+(+(0(),0()),0()),x655) +(0(),+(0(),x664)) <-2|[]- +(+(0(),0()),x664) -3|[]-> +(0(),+(0(),x664)) +(+(0(),+(0(),0())),x664) <-2|0[]- +(+(+(0(),0()),0()),x664) -3| []-> +(+(0(),0()),+(0(),x664)) +(0(),+(0(),x670)) <-2|[]- +(+(0(),0()),x670) -4|[]-> +(0(),+(0(),x670)) +(+(0(),+(0(),x668)),x670) <-2|0[]- +(+(+(0(),0()),x668),x670) -4| []-> +(+(0(),0()),+(x668,x670)) +(0(),+(0(),+(x676,x678))) <-2|[]- +(+(0(),0()),+(x676,x678)) -5| []-> +(+(+(0(),0()),x676),x678) +(x675,+(0(),+(0(),x678))) <-2|1[]- +(x675,+(+(0(),0()),x678)) -5| []-> +(+(x675,+(0(),0())),x678) +(+(0(),+(0(),s(x688))),x690) <-2|0[]- +(+(+(0(),0()),s(x688)),x690) -7| []-> +(+(0(),0()),+(s(x688),x690)) +(0(),+(0(),s(x704))) <-2|[]- +(+(0(),0()),s(x704)) -8|[]-> s(+(+(0(),0()),x704)) +(0(),+(0(),+(s(x754),x755))) <-2|[]- +(+(0(),0()),+(s(x754),x755)) -9| []-> +(+(+(0(),0()),s(x754)),x755) +(0(),+(0(),x813)) <-2|[]- +(+(0(),0()),x813) -10|[]-> +(0(),+(0(),x813)) +(0(),+(0(),+(x871,s(x872)))) <-2|[]- +(+(0(),0()),+(x871,s(x872))) -12| []-> +(+(+(0(),0()),x871),s(x872)) +(x870,+(0(),+(0(),s(x872)))) <-2|1[]- +(x870,+(+(0(),0()),s(x872))) -12| []-> +(+(x870,+(0(),0())),s(x872)) +(0(),+(0(),s(x922))) <-2|[]- +(+(0(),0()),s(x922)) -13|[]-> +(0(),+(0(),s(x922))) +(+(0(),+(0(),x921)),s(x922)) <-2|0[]- +(+(+(0(),0()),x921),s(x922)) -13| []-> +(+(0(),0()),+(x921,s(x922))) +(0(),+(0(),s(x972))) <-2|[]- +(+(0(),0()),s(x972)) -16|[]-> +(0(),+(0(),s(x972))) +(x3497,+(0(),0())) <-3|[]- +(+(x3497,0()),0()) -0|[]-> +(x3497,0()) +(x3499,+(0(),+(0(),x655))) <-3|[]- +(+(x3499,0()),+(0(),x655)) -1| []-> +(+(+(x3499,0()),0()),x655) +(0(),+(0(),x661)) <-3|[]- +(+(0(),0()),x661) -2|[]-> +(0(),+(0(),x661)) +(+(x3503,+(0(),0())),x664) <-3|0[]- +(+(+(x3503,0()),0()),x664) -3| []-> +(+(x3503,0()),+(0(),x664)) +(x667,+(0(),x670)) <-3|[]- +(+(x667,0()),x670) -4|[]-> +(x667,+(0(),x670)) +(+(x3507,+(0(),x668)),x670) <-3|0[]- +(+(+(x3507,0()),x668),x670) -4| []-> +(+(x3507,0()),+(x668,x670)) +(x3509,+(0(),+(x676,x678))) <-3|[]- +(+(x3509,0()),+(x676,x678)) -5| []-> +(+(+(x3509,0()),x676),x678) +(x675,+(x3511,+(0(),x678))) <-3|1[]- +(x675,+(+(x3511,0()),x678)) -5| []-> +(+(x675,+(x3511,0())),x678) +(s(x685),+(0(),x686)) <-3|[]- +(+(s(x685),0()),x686) -6|[]-> +(s(x685),+(0(),x686)) +(+(x3515,+(0(),s(x688))),x690) <-3|0[]- +(+(+(x3515,0()),s(x688)),x690) -7| []-> +(+(x3515,0()),+(s(x688),x690)) +(x3517,+(0(),s(x704))) <-3|[]- +(+(x3517,0()),s(x704)) -8|[]-> s(+(+(x3517,0()),x704)) +(x3519,+(0(),+(s(x754),x755))) <-3|[]- +(+(x3519,0()),+(s(x754),x755)) -9| []-> +(+(+(x3519,0()),s(x754)),x755) +(0(),+(0(),x813)) <-3|[]- +(+(0(),0()),x813) -10|[]-> +(0(),+(0(),x813)) +(s(x844),+(0(),x846)) <-3|[]- +(+(s(x844),0()),x846) -11|[]-> +(s(x844),+(0(),x846)) +(x3525,+(0(),+(x871,s(x872)))) <-3|[]- +(+(x3525,0()),+(x871,s(x872))) -12| []-> +(+(+(x3525,0()),x871),s(x872)) +(x870,+(x3527,+(0(),s(x872)))) <-3|1[]- +(x870,+(+(x3527,0()),s(x872))) -12| []-> +(+(x870,+(x3527,0())),s(x872)) +(x920,+(0(),s(x922))) <-3|[]- +(+(x920,0()),s(x922)) -13|[]-> +(x920,+(0(),s(x922))) +(+(x3531,+(0(),x921)),s(x922)) <-3|0[]- +(+(+(x3531,0()),x921),s(x922)) -13| []-> +(+(x3531,0()),+(x921,s(x922))) +(0(),+(0(),s(x972))) <-3|[]- +(+(0(),0()),s(x972)) -16|[]-> +(0(),+(0(),s(x972))) +(s(x1003),+(0(),s(x1005))) <-3|[]- +(+(s(x1003),0()),s(x1005)) -17| []-> +(s(x1003),+(0(),s(x1005))) +(x3537,+(x3538,0())) <-4|[]- +(+(x3537,x3538),0()) -0|[]-> +(x3537,x3538) +(x3540,+(x3541,+(0(),x655))) <-4|[]- +(+(x3540,x3541),+(0(),x655)) -1| []-> +(+(+(x3540,x3541),0()),x655) +(0(),+(0(),x661)) <-4|[]- +(+(0(),0()),x661) -2|[]-> +(0(),+(0(),x661)) +(x662,+(0(),x664)) <-4|[]- +(+(x662,0()),x664) -3|[]-> +(x662,+(0(),x664)) +(+(x3549,+(x3550,0())),x664) <-4|0[]- +(+(+(x3549,x3550),0()),x664) -3| []-> +(+(x3549,x3550),+(0(),x664)) +(+(x3552,+(x3553,x668)),x670) <-4|0[]- +(+(+(x3552,x3553),x668),x670) -4| []-> +(+(x3552,x3553),+(x668,x670)) +(x3555,+(x3556,+(x676,x678))) <-4|[]- +(+(x3555,x3556),+(x676,x678)) -5| []-> +(+(+(x3555,x3556),x676),x678) +(x675,+(x3558,+(x3559,x678))) <-4|1[]- +(x675,+(+(x3558,x3559),x678)) -5| []-> +(+(x675,+(x3558,x3559)),x678) +(s(x685),+(0(),x686)) <-4|[]- +(+(s(x685),0()),x686) -6|[]-> +(s(x685),+(0(),x686)) +(x687,+(s(x688),x690)) <-4|[]- +(+(x687,s(x688)),x690) -7|[]-> +(x687,+(s(x688),x690)) +(+(x3567,+(x3568,s(x688))),x690) <-4|0[]- +(+(+(x3567,x3568),s(x688)),x690) -7| []-> +(+(x3567,x3568),+(s(x688),x690)) +(x3570,+(x3571,s(x704))) <-4|[]- +(+(x3570,x3571),s(x704)) -8| []-> s(+(+(x3570,x3571),x704)) +(x3573,+(x3574,+(s(x754),x755))) <-4|[]- +(+(x3573,x3574),+(s(x754),x755)) -9| []-> +(+(+(x3573,x3574),s(x754)),x755) +(0(),+(x812,x813)) <-4|[]- +(+(0(),x812),x813) -10|[]-> +(0(),+(x812,x813)) +(s(x844),+(x845,x846)) <-4|[]- +(+(s(x844),x845),x846) -11|[]-> +(s(x844),+(x845,x846)) +(x3582,+(x3583,+(x871,s(x872)))) <-4|[]- +(+(x3582,x3583),+(x871,s(x872))) -12| []-> +(+(+(x3582,x3583),x871),s(x872)) +(x870,+(x3585,+(x3586,s(x872)))) <-4|1[]- +(x870,+(+(x3585,x3586),s(x872))) -12| []-> +(+(x870,+(x3585,x3586)),s(x872)) +(x920,+(x921,s(x922))) <-4|[]- +(+(x920,x921),s(x922)) -13|[]-> +(x920,+(x921,s(x922))) +(+(x3591,+(x3592,x921)),s(x922)) <-4|0[]- +(+(+(x3591,x3592),x921),s(x922)) -13| []-> +(+(x3591,x3592),+(x921,s(x922))) +(0(),+(s(x931),x932)) <-4|[]- +(+(0(),s(x931)),x932) -14|[]-> +(0(),+(s(x931),x932)) +(s(x963),+(s(x964),x965)) <-4|[]- +(+(s(x963),s(x964)),x965) -15| []-> +(s(x963),+(s(x964),x965)) +(0(),+(x971,s(x972))) <-4|[]- +(+(0(),x971),s(x972)) -16|[]-> +(0(),+(x971,s(x972))) +(s(x1003),+(x1004,s(x1005))) <-4|[]- +(+(s(x1003),x1004),s(x1005)) -17| []-> +(s(x1003),+(x1004,s(x1005))) +(+(x654,0()),x655) <-5|[]- +(x654,+(0(),x655)) -1|[]-> +(+(x654,0()),x655) +(x654,+(+(0(),x3610),x3611)) <-5|1[]- +(x654,+(0(),+(x3610,x3611))) -1| []-> +(+(x654,0()),+(x3610,x3611)) +(+(+(0(),0()),x3613),x3614) <-5|[]- +(+(0(),0()),+(x3613,x3614)) -2| []-> +(0(),+(0(),+(x3613,x3614))) +(+(+(x662,0()),x3616),x3617) <-5|[]- +(+(x662,0()),+(x3616,x3617)) -3| []-> +(x662,+(0(),+(x3616,x3617))) +(+(+(x667,x668),x3619),x3620) <-5|[]- +(+(x667,x668),+(x3619,x3620)) -4| []-> +(x667,+(x668,+(x3619,x3620))) +(+(+(x667,x3622),x3623),x670) <-5|0[]- +(+(x667,+(x3622,x3623)),x670) -4| []-> +(x667,+(+(x3622,x3623),x670)) +(x675,+(+(x676,x3625),x3626)) <-5|1[]- +(x675,+(x676,+(x3625,x3626))) -5| []-> +(+(x675,x676),+(x3625,x3626)) +(+(+(s(x685),0()),x3628),x3629) <-5|[]- +(+(s(x685),0()),+(x3628,x3629)) -6| []-> +(s(x685),+(0(),+(x3628,x3629))) +(+(+(x687,s(x688)),x3631),x3632) <-5|[]- +(+(x687,s(x688)),+(x3631,x3632)) -7| []-> +(x687,+(s(x688),+(x3631,x3632))) +(+(x753,s(x754)),x755) <-5|[]- +(x753,+(s(x754),x755)) -9|[]-> +(+(x753,s(x754)),x755) +(x753,+(+(s(x754),x3637),x3638)) <-5|1[]- +(x753,+(s(x754),+(x3637,x3638))) -9| []-> +(+(x753,s(x754)),+(x3637,x3638)) +(+(+(0(),x812),x3640),x3641) <-5|[]- +(+(0(),x812),+(x3640,x3641)) -10| []-> +(0(),+(x812,+(x3640,x3641))) +(+(+(0(),x3643),x3644),x813) <-5|0[]- +(+(0(),+(x3643,x3644)),x813) -10| []-> +(0(),+(+(x3643,x3644),x813)) +(+(+(s(x844),x845),x3646),x3647) <-5|[]- +(+(s(x844),x845),+(x3646,x3647)) -11| []-> +(s(x844),+(x845,+(x3646,x3647))) +(+(+(s(x844),x3649),x3650),x846) <-5|0[]- +(+(s(x844),+(x3649,x3650)),x846) -11| []-> +(s(x844),+(+(x3649,x3650),x846)) +(+(x870,x871),s(x872)) <-5|[]- +(x870,+(x871,s(x872))) -12|[]-> +(+(x870,x871),s(x872)) +(+(+(x920,x3655),x3656),s(x922)) <-5|0[]- +(+(x920,+(x3655,x3656)),s(x922)) -13| []-> +(x920,+(+(x3655,x3656),s(x922))) +(+(+(0(),s(x931)),x3658),x3659) <-5|[]- +(+(0(),s(x931)),+(x3658,x3659)) -14| []-> +(0(),+(s(x931),+(x3658,x3659))) +(+(+(s(x963),s(x964)),x3661),x3662) <-5|[]- +(+(s(x963),s(x964)),+(x3661,x3662)) -15| []-> +(s(x963),+(s(x964),+(x3661,x3662))) +(+(+(0(),x3664),x3665),s(x972)) <-5|0[]- +(+(0(),+(x3664,x3665)),s(x972)) -16| []-> +(0(),+(+(x3664,x3665),s(x972))) +(+(+(s(x1003),x3667),x3668),s(x1005)) <-5|0[]- +(+(s(x1003),+(x3667,x3668)),s(x1005)) -17| []-> +(s(x1003),+(+(x3667,x3668),s(x1005))) +(s(x3669),+(0(),0())) <-6|[]- +(+(s(x3669),0()),0()) -0|[]-> +(s(x3669),0()) +(s(x3671),+(0(),+(0(),x655))) <-6|[]- +(+(s(x3671),0()),+(0(),x655)) -1| []-> +(+(+(s(x3671),0()),0()),x655) +(s(x3673),+(0(),x664)) <-6|[]- +(+(s(x3673),0()),x664) -3|[]-> +(s(x3673),+(0(),x664)) +(+(s(x3675),+(0(),0())),x664) <-6|0[]- +(+(+(s(x3675),0()),0()),x664) -3| []-> +(+(s(x3675),0()),+(0(),x664)) +(s(x3677),+(0(),x670)) <-6|[]- +(+(s(x3677),0()),x670) -4|[]-> +(s(x3677),+(0(),x670)) +(+(s(x3679),+(0(),x668)),x670) <-6|0[]- +(+(+(s(x3679),0()),x668),x670) -4| []-> +(+(s(x3679),0()),+(x668,x670)) +(s(x3681),+(0(),+(x676,x678))) <-6|[]- +(+(s(x3681),0()),+(x676,x678)) -5| []-> +(+(+(s(x3681),0()),x676),x678) +(x675,+(s(x3683),+(0(),x678))) <-6|1[]- +(x675,+(+(s(x3683),0()),x678)) -5| []-> +(+(x675,+(s(x3683),0())),x678) +(+(s(x3685),+(0(),s(x688))),x690) <-6|0[]- +(+(+(s(x3685),0()),s(x688)),x690) -7| []-> +(+(s(x3685),0()),+(s(x688),x690)) +(s(x3687),+(0(),s(x704))) <-6|[]- +(+(s(x3687),0()),s(x704)) -8| []-> s(+(+(s(x3687),0()),x704)) +(s(x3689),+(0(),+(s(x754),x755))) <-6|[]- +(+(s(x3689),0()),+(s(x754),x755)) -9| []-> +(+(+(s(x3689),0()),s(x754)),x755) +(s(x844),+(0(),x846)) <-6|[]- +(+(s(x844),0()),x846) -11|[]-> +(s(x844),+(0(),x846)) +(s(x3693),+(0(),+(x871,s(x872)))) <-6|[]- +(+(s(x3693),0()),+(x871,s(x872))) -12| []-> +(+(+(s(x3693),0()),x871),s(x872)) +(x870,+(s(x3695),+(0(),s(x872)))) <-6|1[]- +(x870,+(+(s(x3695),0()),s(x872))) -12| []-> +(+(x870,+(s(x3695),0())),s(x872)) +(s(x3697),+(0(),s(x922))) <-6|[]- +(+(s(x3697),0()),s(x922)) -13| []-> +(s(x3697),+(0(),s(x922))) +(+(s(x3699),+(0(),x921)),s(x922)) <-6|0[]- +(+(+(s(x3699),0()),x921),s(x922)) -13| []-> +(+(s(x3699),0()),+(x921,s(x922))) +(s(x1003),+(0(),s(x1005))) <-6|[]- +(+(s(x1003),0()),s(x1005)) -17| []-> +(s(x1003),+(0(),s(x1005))) +(x3703,+(s(x3704),0())) <-7|[]- +(+(x3703,s(x3704)),0()) -0|[]-> +(x3703,s(x3704)) +(x3706,+(s(x3707),+(0(),x655))) <-7|[]- +(+(x3706,s(x3707)),+(0(),x655)) -1| []-> +(+(+(x3706,s(x3707)),0()),x655) +(+(x3709,+(s(x3710),0())),x664) <-7|0[]- +(+(+(x3709,s(x3710)),0()),x664) -3| []-> +(+(x3709,s(x3710)),+(0(),x664)) +(x667,+(s(x3713),x670)) <-7|[]- +(+(x667,s(x3713)),x670) -4|[]-> +(x667,+(s(x3713),x670)) +(+(x3715,+(s(x3716),x668)),x670) <-7|0[]- +(+(+(x3715,s(x3716)),x668),x670) -4| []-> +(+(x3715,s(x3716)),+(x668,x670)) +(x3718,+(s(x3719),+(x676,x678))) <-7|[]- +(+(x3718,s(x3719)),+(x676,x678)) -5| []-> +(+(+(x3718,s(x3719)),x676),x678) +(x675,+(x3721,+(s(x3722),x678))) <-7|1[]- +(x675,+(+(x3721,s(x3722)),x678)) -5| []-> +(+(x675,+(x3721,s(x3722))),x678) +(+(x3724,+(s(x3725),s(x688))),x690) <-7|0[]- +(+(+(x3724,s(x3725)),s(x688)),x690) -7| []-> +(+(x3724,s(x3725)),+(s(x688),x690)) +(x3727,+(s(x3728),s(x704))) <-7|[]- +(+(x3727,s(x3728)),s(x704)) -8| []-> s(+(+(x3727,s(x3728)),x704)) +(x3730,+(s(x3731),+(s(x754),x755))) <-7|[]- +(+(x3730,s(x3731)),+(s(x754),x755)) -9| []-> +(+(+(x3730,s(x3731)),s(x754)),x755) +(0(),+(s(x3734),x813)) <-7|[]- +(+(0(),s(x3734)),x813) -10|[]-> +(0(),+(s(x3734),x813)) +(s(x844),+(s(x3737),x846)) <-7|[]- +(+(s(x844),s(x3737)),x846) -11| []-> +(s(x844),+(s(x3737),x846)) +(x3739,+(s(x3740),+(x871,s(x872)))) <-7|[]- +(+(x3739,s(x3740)),+(x871,s(x872))) -12| []-> +(+(+(x3739,s(x3740)),x871),s(x872)) +(x870,+(x3742,+(s(x3743),s(x872)))) <-7|1[]- +(x870,+(+(x3742,s(x3743)),s(x872))) -12| []-> +(+(x870,+(x3742,s(x3743))),s(x872)) +(x920,+(s(x3746),s(x922))) <-7|[]- +(+(x920,s(x3746)),s(x922)) -13| []-> +(x920,+(s(x3746),s(x922))) +(+(x3748,+(s(x3749),x921)),s(x922)) <-7|0[]- +(+(+(x3748,s(x3749)),x921),s(x922)) -13| []-> +(+(x3748,s(x3749)),+(x921,s(x922))) +(0(),+(s(x931),x932)) <-7|[]- +(+(0(),s(x931)),x932) -14|[]-> +(0(),+(s(x931),x932)) +(s(x963),+(s(x964),x965)) <-7|[]- +(+(s(x963),s(x964)),x965) -15| []-> +(s(x963),+(s(x964),x965)) +(0(),+(s(x3758),s(x972))) <-7|[]- +(+(0(),s(x3758)),s(x972)) -16| []-> +(0(),+(s(x3758),s(x972))) +(s(x1003),+(s(x3761),s(x1005))) <-7|[]- +(+(s(x1003),s(x3761)),s(x1005)) -17| []-> +(s(x1003),+(s(x3761),s(x1005))) +(x654,s(+(0(),x3764))) <-8|1[]- +(x654,+(0(),s(x3764))) -1|[]-> +(+(x654,0()),s(x3764)) s(+(+(0(),0()),x3766)) <-8|[]- +(+(0(),0()),s(x3766)) -2|[]-> +(0(),+(0(),s(x3766))) s(+(+(x662,0()),x3768)) <-8|[]- +(+(x662,0()),s(x3768)) -3|[]-> +(x662,+(0(),s(x3768))) s(+(+(x667,x668),x3770)) <-8|[]- +(+(x667,x668),s(x3770)) -4|[]-> +(x667,+(x668,s(x3770))) +(s(+(x667,x3772)),x670) <-8|0[]- +(+(x667,s(x3772)),x670) -4| []-> +(x667,+(s(x3772),x670)) +(x675,s(+(x676,x3774))) <-8|1[]- +(x675,+(x676,s(x3774))) -5| []-> +(+(x675,x676),s(x3774)) s(+(+(s(x685),0()),x3776)) <-8|[]- +(+(s(x685),0()),s(x3776)) -6| []-> +(s(x685),+(0(),s(x3776))) s(+(+(x687,s(x688)),x3778)) <-8|[]- +(+(x687,s(x688)),s(x3778)) -7| []-> +(x687,+(s(x688),s(x3778))) +(s(+(x687,x688)),x690) <-8|0[]- +(+(x687,s(x688)),x690) -7|[]-> +(x687,+(s(x688),x690)) +(x753,s(+(s(x754),x3782))) <-8|1[]- +(x753,+(s(x754),s(x3782))) -9| []-> +(+(x753,s(x754)),s(x3782)) s(+(+(0(),x812),x3784)) <-8|[]- +(+(0(),x812),s(x3784)) -10|[]-> +(0(),+(x812,s(x3784))) +(s(+(0(),x3786)),x813) <-8|0[]- +(+(0(),s(x3786)),x813) -10|[]-> +(0(),+(s(x3786),x813)) s(+(+(s(x844),x845),x3788)) <-8|[]- +(+(s(x844),x845),s(x3788)) -11| []-> +(s(x844),+(x845,s(x3788))) +(s(+(s(x844),x3790)),x846) <-8|0[]- +(+(s(x844),s(x3790)),x846) -11| []-> +(s(x844),+(s(x3790),x846)) +(x870,s(+(x871,x872))) <-8|1[]- +(x870,+(x871,s(x872))) -12|[]-> +(+(x870,x871),s(x872)) s(+(+(x920,x921),x922)) <-8|[]- +(+(x920,x921),s(x922)) -13|[]-> +(x920,+(x921,s(x922))) +(s(+(x920,x3796)),s(x922)) <-8|0[]- +(+(x920,s(x3796)),s(x922)) -13| []-> +(x920,+(s(x3796),s(x922))) s(+(+(0(),s(x931)),x3798)) <-8|[]- +(+(0(),s(x931)),s(x3798)) -14| []-> +(0(),+(s(x931),s(x3798))) +(s(+(0(),x931)),x932) <-8|0[]- +(+(0(),s(x931)),x932) -14|[]-> +(0(),+(s(x931),x932)) s(+(+(s(x963),s(x964)),x3802)) <-8|[]- +(+(s(x963),s(x964)),s(x3802)) -15| []-> +(s(x963),+(s(x964),s(x3802))) +(s(+(s(x963),x964)),x965) <-8|0[]- +(+(s(x963),s(x964)),x965) -15| []-> +(s(x963),+(s(x964),x965)) s(+(+(0(),x971),x972)) <-8|[]- +(+(0(),x971),s(x972)) -16|[]-> +(0(),+(x971,s(x972))) +(s(+(0(),x3808)),s(x972)) <-8|0[]- +(+(0(),s(x3808)),s(x972)) -16| []-> +(0(),+(s(x3808),s(x972))) s(+(+(s(x1003),x1004),x1005)) <-8|[]- +(+(s(x1003),x1004),s(x1005)) -17| []-> +(s(x1003),+(x1004,s(x1005))) +(s(+(s(x1003),x3812)),s(x1005)) <-8|0[]- +(+(s(x1003),s(x3812)),s(x1005)) -17| []-> +(s(x1003),+(s(x3812),s(x1005))) +(x654,+(+(0(),s(x3814)),x3815)) <-9|1[]- +(x654,+(0(),+(s(x3814),x3815))) -1| []-> +(+(x654,0()),+(s(x3814),x3815)) +(+(+(0(),0()),s(x3817)),x3818) <-9|[]- +(+(0(),0()),+(s(x3817),x3818)) -2| []-> +(0(),+(0(),+(s(x3817),x3818))) +(+(+(x662,0()),s(x3820)),x3821) <-9|[]- +(+(x662,0()),+(s(x3820),x3821)) -3| []-> +(x662,+(0(),+(s(x3820),x3821))) +(+(+(x667,x668),s(x3823)),x3824) <-9|[]- +(+(x667,x668),+(s(x3823),x3824)) -4| []-> +(x667,+(x668,+(s(x3823),x3824))) +(+(+(x667,s(x3826)),x3827),x670) <-9|0[]- +(+(x667,+(s(x3826),x3827)),x670) -4| []-> +(x667,+(+(s(x3826),x3827),x670)) +(+(x675,s(x3829)),x678) <-9|[]- +(x675,+(s(x3829),x678)) -5|[]-> +(+(x675,s(x3829)),x678) +(x675,+(+(x676,s(x3832)),x3833)) <-9|1[]- +(x675,+(x676,+(s(x3832),x3833))) -5| []-> +(+(x675,x676),+(s(x3832),x3833)) +(+(+(s(x685),0()),s(x3835)),x3836) <-9|[]- +(+(s(x685),0()),+(s(x3835),x3836)) -6| []-> +(s(x685),+(0(),+(s(x3835),x3836))) +(+(+(x687,s(x688)),s(x3838)),x3839) <-9|[]- +(+(x687,s(x688)),+(s(x3838),x3839)) -7| []-> +(x687,+(s(x688),+(s(x3838),x3839))) +(x753,+(+(s(x754),s(x3841)),x3842)) <-9|1[]- +(x753,+(s(x754),+(s(x3841),x3842))) -9| []-> +(+(x753,s(x754)),+(s(x3841),x3842)) +(+(+(0(),x812),s(x3844)),x3845) <-9|[]- +(+(0(),x812),+(s(x3844),x3845)) -10| []-> +(0(),+(x812,+(s(x3844),x3845))) +(+(+(0(),s(x3847)),x3848),x813) <-9|0[]- +(+(0(),+(s(x3847),x3848)),x813) -10| []-> +(0(),+(+(s(x3847),x3848),x813)) +(+(+(s(x844),x845),s(x3850)),x3851) <-9|[]- +(+(s(x844),x845),+(s(x3850),x3851)) -11| []-> +(s(x844),+(x845,+(s(x3850),x3851))) +(+(+(s(x844),s(x3853)),x3854),x846) <-9|0[]- +(+(s(x844),+(s(x3853),x3854)),x846) -11| []-> +(s(x844),+(+(s(x3853),x3854),x846)) +(+(x870,s(x3856)),s(x872)) <-9|[]- +(x870,+(s(x3856),s(x872))) -12| []-> +(+(x870,s(x3856)),s(x872)) +(+(+(x920,s(x3859)),x3860),s(x922)) <-9|0[]- +(+(x920,+(s(x3859),x3860)),s(x922)) -13| []-> +(x920,+(+(s(x3859),x3860),s(x922))) +(+(+(0(),s(x931)),s(x3862)),x3863) <-9|[]- +(+(0(),s(x931)),+(s(x3862),x3863)) -14| []-> +(0(),+(s(x931),+(s(x3862),x3863))) +(+(+(s(x963),s(x964)),s(x3865)),x3866) <-9|[]- +(+(s(x963),s(x964)),+(s(x3865),x3866)) -15| []-> +(s(x963), +(s(x964),+(s(x3865),x3866))) +(+(+(0(),s(x3868)),x3869),s(x972)) <-9|0[]- +(+(0(),+(s(x3868),x3869)),s(x972)) -16| []-> +(0(),+(+(s(x3868),x3869),s(x972))) +(+(+(s(x1003),s(x3871)),x3872),s(x1005)) <-9|0[]- +(+(s(x1003),+(s(x3871),x3872)), s(x1005)) -17| []-> +(s(x1003), +(+(s(x3871),x3872),s(x1005))) +(0(),+(x3873,0())) <-10|[]- +(+(0(),x3873),0()) -0|[]-> +(0(),x3873) +(0(),+(x3875,+(0(),x655))) <-10|[]- +(+(0(),x3875),+(0(),x655)) -1| []-> +(+(+(0(),x3875),0()),x655) +(0(),+(0(),x661)) <-10|[]- +(+(0(),0()),x661) -2|[]-> +(0(),+(0(),x661)) +(0(),+(0(),x664)) <-10|[]- +(+(0(),0()),x664) -3|[]-> +(0(),+(0(),x664)) +(+(0(),+(x3881,0())),x664) <-10|0[]- +(+(+(0(),x3881),0()),x664) -3| []-> +(+(0(),x3881),+(0(),x664)) +(0(),+(x668,x670)) <-10|[]- +(+(0(),x668),x670) -4|[]-> +(0(),+(x668,x670)) +(+(0(),+(x3885,x668)),x670) <-10|0[]- +(+(+(0(),x3885),x668),x670) -4| []-> +(+(0(),x3885),+(x668,x670)) +(0(),+(x3887,+(x676,x678))) <-10|[]- +(+(0(),x3887),+(x676,x678)) -5| []-> +(+(+(0(),x3887),x676),x678) +(x675,+(0(),+(x3889,x678))) <-10|1[]- +(x675,+(+(0(),x3889),x678)) -5| []-> +(+(x675,+(0(),x3889)),x678) +(0(),+(s(x688),x690)) <-10|[]- +(+(0(),s(x688)),x690) -7|[]-> +(0(),+(s(x688),x690)) +(+(0(),+(x3893,s(x688))),x690) <-10|0[]- +(+(+(0(),x3893),s(x688)),x690) -7| []-> +(+(0(),x3893),+(s(x688),x690)) +(0(),+(x3895,s(x704))) <-10|[]- +(+(0(),x3895),s(x704)) -8|[]-> s(+(+(0(),x3895),x704)) +(0(),+(x3897,+(s(x754),x755))) <-10|[]- +(+(0(),x3897),+(s(x754),x755)) -9| []-> +(+(+(0(),x3897),s(x754)),x755) +(0(),+(x3899,+(x871,s(x872)))) <-10|[]- +(+(0(),x3899),+(x871,s(x872))) -12| []-> +(+(+(0(),x3899),x871),s(x872)) +(x870,+(0(),+(x3901,s(x872)))) <-10|1[]- +(x870,+(+(0(),x3901),s(x872))) -12| []-> +(+(x870,+(0(),x3901)),s(x872)) +(0(),+(x921,s(x922))) <-10|[]- +(+(0(),x921),s(x922)) -13|[]-> +(0(),+(x921,s(x922))) +(+(0(),+(x3905,x921)),s(x922)) <-10|0[]- +(+(+(0(),x3905),x921),s(x922)) -13| []-> +(+(0(),x3905),+(x921,s(x922))) +(0(),+(s(x931),x932)) <-10|[]- +(+(0(),s(x931)),x932) -14|[]-> +(0(),+(s(x931),x932)) +(0(),+(x971,s(x972))) <-10|[]- +(+(0(),x971),s(x972)) -16|[]-> +(0(),+(x971,s(x972))) +(s(x3911),+(x3912,0())) <-11|[]- +(+(s(x3911),x3912),0()) -0|[]-> +(s(x3911),x3912) +(s(x3914),+(x3915,+(0(),x655))) <-11|[]- +(+(s(x3914),x3915),+(0(),x655)) -1| []-> +(+(+(s(x3914),x3915),0()),x655) +(s(x3917),+(0(),x664)) <-11|[]- +(+(s(x3917),0()),x664) -3|[]-> +(s(x3917),+(0(),x664)) +(+(s(x3920),+(x3921,0())),x664) <-11|0[]- +(+(+(s(x3920),x3921),0()),x664) -3| []-> +(+(s(x3920),x3921),+(0(),x664)) +(s(x3923),+(x668,x670)) <-11|[]- +(+(s(x3923),x668),x670) -4| []-> +(s(x3923),+(x668,x670)) +(+(s(x3926),+(x3927,x668)),x670) <-11|0[]- +(+(+(s(x3926),x3927),x668),x670) -4| []-> +(+(s(x3926),x3927),+(x668,x670)) +(s(x3929),+(x3930,+(x676,x678))) <-11|[]- +(+(s(x3929),x3930),+(x676,x678)) -5| []-> +(+(+(s(x3929),x3930),x676),x678) +(x675,+(s(x3932),+(x3933,x678))) <-11|1[]- +(x675,+(+(s(x3932),x3933),x678)) -5| []-> +(+(x675,+(s(x3932),x3933)),x678) +(s(x685),+(0(),x686)) <-11|[]- +(+(s(x685),0()),x686) -6|[]-> +(s(x685),+(0(),x686)) +(s(x3938),+(s(x688),x690)) <-11|[]- +(+(s(x3938),s(x688)),x690) -7| []-> +(s(x3938),+(s(x688),x690)) +(+(s(x3941),+(x3942,s(x688))),x690) <-11|0[]- +(+(+(s(x3941),x3942),s(x688)),x690) -7| []-> +(+(s(x3941),x3942),+(s(x688),x690)) +(s(x3944),+(x3945,s(x704))) <-11|[]- +(+(s(x3944),x3945),s(x704)) -8| []-> s(+(+(s(x3944),x3945),x704)) +(s(x3947),+(x3948,+(s(x754),x755))) <-11|[]- +(+(s(x3947),x3948),+(s(x754),x755)) -9| []-> +(+(+(s(x3947),x3948),s(x754)),x755) +(s(x3950),+(x3951,+(x871,s(x872)))) <-11|[]- +(+(s(x3950),x3951),+(x871,s(x872))) -12| []-> +(+(+(s(x3950),x3951),x871),s(x872)) +(x870,+(s(x3953),+(x3954,s(x872)))) <-11|1[]- +(x870,+(+(s(x3953),x3954),s(x872))) -12| []-> +(+(x870,+(s(x3953),x3954)),s(x872)) +(s(x3956),+(x921,s(x922))) <-11|[]- +(+(s(x3956),x921),s(x922)) -13| []-> +(s(x3956),+(x921,s(x922))) +(+(s(x3959),+(x3960,x921)),s(x922)) <-11|0[]- +(+(+(s(x3959),x3960),x921),s(x922)) -13| []-> +(+(s(x3959),x3960),+(x921,s(x922))) +(s(x963),+(s(x964),x965)) <-11|[]- +(+(s(x963),s(x964)),x965) -15| []-> +(s(x963),+(s(x964),x965)) +(s(x1003),+(x1004,s(x1005))) <-11|[]- +(+(s(x1003),x1004),s(x1005)) -17| []-> +(s(x1003),+(x1004,s(x1005))) +(+(x654,0()),s(x3970)) <-12|[]- +(x654,+(0(),s(x3970))) -1|[]-> +(+(x654,0()),s(x3970)) +(x654,+(+(0(),x3972),s(x3973))) <-12|1[]- +(x654,+(0(),+(x3972,s(x3973)))) -1| []-> +(+(x654,0()),+(x3972,s(x3973))) +(+(+(0(),0()),x3975),s(x3976)) <-12|[]- +(+(0(),0()),+(x3975,s(x3976))) -2| []-> +(0(),+(0(),+(x3975,s(x3976)))) +(+(+(x662,0()),x3978),s(x3979)) <-12|[]- +(+(x662,0()),+(x3978,s(x3979))) -3| []-> +(x662,+(0(),+(x3978,s(x3979)))) +(+(+(x667,x668),x3981),s(x3982)) <-12|[]- +(+(x667,x668),+(x3981,s(x3982))) -4| []-> +(x667,+(x668,+(x3981,s(x3982)))) +(+(+(x667,x3984),s(x3985)),x670) <-12|0[]- +(+(x667,+(x3984,s(x3985))),x670) -4| []-> +(x667,+(+(x3984,s(x3985)),x670)) +(+(x675,x676),s(x3988)) <-12|[]- +(x675,+(x676,s(x3988))) -5| []-> +(+(x675,x676),s(x3988)) +(x675,+(+(x676,x3990),s(x3991))) <-12|1[]- +(x675,+(x676,+(x3990,s(x3991)))) -5| []-> +(+(x675,x676),+(x3990,s(x3991))) +(+(+(s(x685),0()),x3993),s(x3994)) <-12|[]- +(+(s(x685),0()),+(x3993,s(x3994))) -6| []-> +(s(x685),+(0(),+(x3993,s(x3994)))) +(+(+(x687,s(x688)),x3996),s(x3997)) <-12|[]- +(+(x687,s(x688)),+(x3996,s(x3997))) -7| []-> +(x687,+(s(x688),+(x3996,s(x3997)))) +(+(x753,s(x754)),s(x4000)) <-12|[]- +(x753,+(s(x754),s(x4000))) -9| []-> +(+(x753,s(x754)),s(x4000)) +(x753,+(+(s(x754),x4002),s(x4003))) <-12|1[]- +(x753,+(s(x754),+(x4002,s(x4003)))) -9| []-> +(+(x753,s(x754)),+(x4002,s(x4003))) +(+(+(0(),x812),x4005),s(x4006)) <-12|[]- +(+(0(),x812),+(x4005,s(x4006))) -10| []-> +(0(),+(x812,+(x4005,s(x4006)))) +(+(+(0(),x4008),s(x4009)),x813) <-12|0[]- +(+(0(),+(x4008,s(x4009))),x813) -10| []-> +(0(),+(+(x4008,s(x4009)),x813)) +(+(+(s(x844),x845),x4011),s(x4012)) <-12|[]- +(+(s(x844),x845),+(x4011,s(x4012))) -11| []-> +(s(x844),+(x845,+(x4011,s(x4012)))) +(+(+(s(x844),x4014),s(x4015)),x846) <-12|0[]- +(+(s(x844),+(x4014,s(x4015))),x846) -11| []-> +(s(x844),+(+(x4014,s(x4015)),x846)) +(+(+(x920,x4017),s(x4018)),s(x922)) <-12|0[]- +(+(x920,+(x4017,s(x4018))),s(x922)) -13| []-> +(x920,+(+(x4017,s(x4018)),s(x922))) +(+(+(0(),s(x931)),x4020),s(x4021)) <-12|[]- +(+(0(),s(x931)),+(x4020,s(x4021))) -14| []-> +(0(),+(s(x931),+(x4020,s(x4021)))) +(+(+(s(x963),s(x964)),x4023),s(x4024)) <-12|[]- +(+(s(x963),s(x964)),+(x4023,s(x4024))) -15| []-> +(s(x963), +(s(x964),+(x4023,s(x4024)))) +(+(+(0(),x4026),s(x4027)),s(x972)) <-12|0[]- +(+(0(),+(x4026,s(x4027))),s(x972)) -16| []-> +(0(),+(+(x4026,s(x4027)),s(x972))) +(+(+(s(x1003),x4029),s(x4030)),s(x1005)) <-12|0[]- +(+(s(x1003),+(x4029,s(x4030))), s(x1005)) -17| []-> +(s(x1003), + (+(x4029,s(x4030)),s(x1005))) +(0(),+(0(),s(x4033))) <-13|[]- +(+(0(),0()),s(x4033)) -2|[]-> +(0(),+(0(),s(x4033))) +(x662,+(0(),s(x4036))) <-13|[]- +(+(x662,0()),s(x4036)) -3|[]-> +(x662,+(0(),s(x4036))) +(x667,+(x668,s(x4039))) <-13|[]- +(+(x667,x668),s(x4039)) -4| []-> +(x667,+(x668,s(x4039))) +(+(x4040,+(x4041,s(x4042))),x670) <-13|0[]- +(+(+(x4040,x4041),s(x4042)),x670) -4| []-> +(+(x4040,x4041),+(s(x4042),x670)) +(x675,+(x4043,+(x4044,s(x4045)))) <-13|1[]- +(x675,+(+(x4043,x4044),s(x4045))) -5| []-> +(+(x675,+(x4043,x4044)),s(x4045)) +(s(x685),+(0(),s(x4048))) <-13|[]- +(+(s(x685),0()),s(x4048)) -6| []-> +(s(x685),+(0(),s(x4048))) +(x687,+(s(x688),s(x4051))) <-13|[]- +(+(x687,s(x688)),s(x4051)) -7| []-> +(x687,+(s(x688),s(x4051))) +(+(x4052,+(x4053,s(x688))),x690) <-13|0[]- +(+(+(x4052,x4053),s(x688)),x690) -7| []-> +(+(x4052,x4053),+(s(x688),x690)) +(x4055,+(x4056,s(x704))) <-13|[]- +(+(x4055,x4056),s(x704)) -8| []-> s(+(+(x4055,x4056),x704)) +(0(),+(x812,s(x4060))) <-13|[]- +(+(0(),x812),s(x4060)) -10|[]-> +(0(),+(x812,s(x4060))) +(s(x844),+(x845,s(x4063))) <-13|[]- +(+(s(x844),x845),s(x4063)) -11| []-> +(s(x844),+(x845,s(x4063))) +(x870,+(x4064,+(x4065,s(x872)))) <-13|1[]- +(x870,+(+(x4064,x4065),s(x872))) -12| []-> +(+(x870,+(x4064,x4065)),s(x872)) +(+(x4067,+(x4068,s(x4069))),s(x922)) <-13|0[]- +(+(+(x4067,x4068),s(x4069)),s(x922)) -13| []-> +(+(x4067,x4068),+(s(x4069),s(x922))) +(0(),+(s(x931),s(x4072))) <-13|[]- +(+(0(),s(x931)),s(x4072)) -14| []-> +(0(),+(s(x931),s(x4072))) +(s(x963),+(s(x964),s(x4075))) <-13|[]- +(+(s(x963),s(x964)),s(x4075)) -15| []-> +(s(x963),+(s(x964),s(x4075))) +(0(),+(x971,s(x972))) <-13|[]- +(+(0(),x971),s(x972)) -16|[]-> +(0(),+(x971,s(x972))) +(s(x1003),+(x1004,s(x1005))) <-13|[]- +(+(s(x1003),x1004),s(x1005)) -17| []-> +(s(x1003),+(x1004,s(x1005))) +(0(),+(s(x4082),0())) <-14|[]- +(+(0(),s(x4082)),0()) -0|[]-> +(0(),s(x4082)) +(0(),+(s(x4084),+(0(),x655))) <-14|[]- +(+(0(),s(x4084)),+(0(),x655)) -1| []-> +(+(+(0(),s(x4084)),0()),x655) +(+(0(),+(s(x4086),0())),x664) <-14|0[]- +(+(+(0(),s(x4086)),0()),x664) -3| []-> +(+(0(),s(x4086)),+(0(),x664)) +(0(),+(s(x4088),x670)) <-14|[]- +(+(0(),s(x4088)),x670) -4|[]-> +(0(),+(s(x4088),x670)) +(+(0(),+(s(x4090),x668)),x670) <-14|0[]- +(+(+(0(),s(x4090)),x668),x670) -4| []-> +(+(0(),s(x4090)),+(x668,x670)) +(0(),+(s(x4092),+(x676,x678))) <-14|[]- +(+(0(),s(x4092)),+(x676,x678)) -5| []-> +(+(+(0(),s(x4092)),x676),x678) +(x675,+(0(),+(s(x4094),x678))) <-14|1[]- +(x675,+(+(0(),s(x4094)),x678)) -5| []-> +(+(x675,+(0(),s(x4094))),x678) +(0(),+(s(x688),x690)) <-14|[]- +(+(0(),s(x688)),x690) -7|[]-> +(0(),+(s(x688),x690)) +(+(0(),+(s(x4098),s(x688))),x690) <-14|0[]- +(+(+(0(),s(x4098)),s(x688)),x690) -7| []-> +(+(0(),s(x4098)),+(s(x688),x690)) +(0(),+(s(x4100),s(x704))) <-14|[]- +(+(0(),s(x4100)),s(x704)) -8| []-> s(+(+(0(),s(x4100)),x704)) +(0(),+(s(x4102),+(s(x754),x755))) <-14|[]- +(+(0(),s(x4102)),+(s(x754),x755)) -9| []-> +(+(+(0(),s(x4102)),s(x754)),x755) +(0(),+(s(x4104),x813)) <-14|[]- +(+(0(),s(x4104)),x813) -10|[]-> +(0(),+(s(x4104),x813)) +(0(),+(s(x4106),+(x871,s(x872)))) <-14|[]- +(+(0(),s(x4106)),+(x871,s(x872))) -12| []-> +(+(+(0(),s(x4106)),x871),s(x872)) +(x870,+(0(),+(s(x4108),s(x872)))) <-14|1[]- +(x870,+(+(0(),s(x4108)),s(x872))) -12| []-> +(+(x870,+(0(),s(x4108))),s(x872)) +(0(),+(s(x4110),s(x922))) <-14|[]- +(+(0(),s(x4110)),s(x922)) -13| []-> +(0(),+(s(x4110),s(x922))) +(+(0(),+(s(x4112),x921)),s(x922)) <-14|0[]- +(+(+(0(),s(x4112)),x921),s(x922)) -13| []-> +(+(0(),s(x4112)),+(x921,s(x922))) +(0(),+(s(x4114),s(x972))) <-14|[]- +(+(0(),s(x4114)),s(x972)) -16| []-> +(0(),+(s(x4114),s(x972))) +(s(x4116),+(s(x4117),0())) <-15|[]- +(+(s(x4116),s(x4117)),0()) -0| []-> +(s(x4116),s(x4117)) +(s(x4119),+(s(x4120),+(0(),x655))) <-15|[]- +(+(s(x4119),s(x4120)),+(0(),x655)) -1| []-> +(+(+(s(x4119),s(x4120)),0()),x655) +(+(s(x4122),+(s(x4123),0())),x664) <-15|0[]- +(+(+(s(x4122),s(x4123)),0()),x664) -3| []-> +(+(s(x4122),s(x4123)),+(0(),x664)) +(s(x4125),+(s(x4126),x670)) <-15|[]- +(+(s(x4125),s(x4126)),x670) -4| []-> +(s(x4125),+(s(x4126),x670)) +(+(s(x4128),+(s(x4129),x668)),x670) <-15|0[]- +(+(+(s(x4128),s(x4129)),x668),x670) -4| []-> +(+(s(x4128),s(x4129)),+(x668,x670)) +(s(x4131),+(s(x4132),+(x676,x678))) <-15|[]- +(+(s(x4131),s(x4132)),+(x676,x678)) -5| []-> +(+(+(s(x4131),s(x4132)),x676),x678) +(x675,+(s(x4134),+(s(x4135),x678))) <-15|1[]- +(x675,+(+(s(x4134),s(x4135)),x678)) -5| []-> +(+(x675,+(s(x4134),s(x4135))),x678) +(s(x4137),+(s(x688),x690)) <-15|[]- +(+(s(x4137),s(x688)),x690) -7| []-> +(s(x4137),+(s(x688),x690)) +(+(s(x4140),+(s(x4141),s(x688))),x690) <-15|0[]- +(+(+(s(x4140),s(x4141)),s(x688)),x690) -7| []-> +(+(s(x4140),s(x4141)), +(s(x688),x690)) +(s(x4143),+(s(x4144),s(x704))) <-15|[]- +(+(s(x4143),s(x4144)),s(x704)) -8| []-> s(+(+(s(x4143),s(x4144)),x704)) +(s(x4146),+(s(x4147),+(s(x754),x755))) <-15|[]- +(+(s(x4146),s(x4147)),+(s(x754),x755)) -9| []-> +(+(+(s(x4146),s(x4147)),s(x754)), x755) +(s(x844),+(s(x4150),x846)) <-15|[]- +(+(s(x844),s(x4150)),x846) -11| []-> +(s(x844),+(s(x4150),x846)) +(s(x4152),+(s(x4153),+(x871,s(x872)))) <-15|[]- +(+(s(x4152),s(x4153)),+(x871,s(x872))) -12| []-> +(+(+(s(x4152),s(x4153)),x871), s(x872)) +(x870,+(s(x4155),+(s(x4156),s(x872)))) <-15|1[]- +(x870,+(+(s(x4155),s(x4156)),s(x872))) -12| []-> +(+(x870,+(s(x4155),s(x4156))), s(x872)) +(s(x4158),+(s(x4159),s(x922))) <-15|[]- +(+(s(x4158),s(x4159)),s(x922)) -13| []-> +(s(x4158),+(s(x4159),s(x922))) +(+(s(x4161),+(s(x4162),x921)),s(x922)) <-15|0[]- +(+(+(s(x4161),s(x4162)),x921),s(x922)) -13| []-> +(+(s(x4161),s(x4162)), +(x921,s(x922))) +(s(x1003),+(s(x4165),s(x1005))) <-15|[]- +(+(s(x1003),s(x4165)),s(x1005)) -17| []-> +(s(x1003),+(s(x4165),s(x1005))) +(0(),+(0(),s(x4168))) <-16|[]- +(+(0(),0()),s(x4168)) -2|[]-> +(0(),+(0(),s(x4168))) +(0(),+(0(),s(x4170))) <-16|[]- +(+(0(),0()),s(x4170)) -3|[]-> +(0(),+(0(),s(x4170))) +(0(),+(x668,s(x4172))) <-16|[]- +(+(0(),x668),s(x4172)) -4|[]-> +(0(),+(x668,s(x4172))) +(+(0(),+(x4173,s(x4174))),x670) <-16|0[]- +(+(+(0(),x4173),s(x4174)),x670) -4| []-> +(+(0(),x4173),+(s(x4174),x670)) +(x675,+(0(),+(x4175,s(x4176)))) <-16|1[]- +(x675,+(+(0(),x4175),s(x4176))) -5| []-> +(+(x675,+(0(),x4175)),s(x4176)) +(0(),+(s(x688),s(x4178))) <-16|[]- +(+(0(),s(x688)),s(x4178)) -7| []-> +(0(),+(s(x688),s(x4178))) +(+(0(),+(x4179,s(x688))),x690) <-16|0[]- +(+(+(0(),x4179),s(x688)),x690) -7| []-> +(+(0(),x4179),+(s(x688),x690)) +(0(),+(x4181,s(x704))) <-16|[]- +(+(0(),x4181),s(x704)) -8|[]-> s(+(+(0(),x4181),x704)) +(0(),+(x812,s(x4184))) <-16|[]- +(+(0(),x812),s(x4184)) -10|[]-> +(0(),+(x812,s(x4184))) +(x870,+(0(),+(x4185,s(x872)))) <-16|1[]- +(x870,+(+(0(),x4185),s(x872))) -12| []-> +(+(x870,+(0(),x4185)),s(x872)) +(0(),+(x921,s(x922))) <-16|[]- +(+(0(),x921),s(x922)) -13|[]-> +(0(),+(x921,s(x922))) +(+(0(),+(x4189,s(x4190))),s(x922)) <-16|0[]- +(+(+(0(),x4189),s(x4190)),s(x922)) -13| []-> +(+(0(),x4189),+(s(x4190),s(x922))) +(0(),+(s(x931),s(x4192))) <-16|[]- +(+(0(),s(x931)),s(x4192)) -14| []-> +(0(),+(s(x931),s(x4192))) +(s(x4193),+(0(),s(x4195))) <-17|[]- +(+(s(x4193),0()),s(x4195)) -3| []-> +(s(x4193),+(0(),s(x4195))) +(s(x4196),+(x668,s(x4198))) <-17|[]- +(+(s(x4196),x668),s(x4198)) -4| []-> +(s(x4196),+(x668,s(x4198))) +(+(s(x4199),+(x4200,s(x4201))),x670) <-17|0[]- +(+(+(s(x4199),x4200),s(x4201)),x670) -4| []-> +(+(s(x4199),x4200),+(s(x4201),x670)) +(x675,+(s(x4202),+(x4203,s(x4204)))) <-17|1[]- +(x675,+(+(s(x4202),x4203),s(x4204))) -5| []-> +(+(x675,+(s(x4202),x4203)),s(x4204)) +(s(x685),+(0(),s(x4207))) <-17|[]- +(+(s(x685),0()),s(x4207)) -6| []-> +(s(x685),+(0(),s(x4207))) +(s(x4208),+(s(x688),s(x4210))) <-17|[]- +(+(s(x4208),s(x688)),s(x4210)) -7| []-> +(s(x4208),+(s(x688),s(x4210))) +(+(s(x4211),+(x4212,s(x688))),x690) <-17|0[]- +(+(+(s(x4211),x4212),s(x688)),x690) -7| []-> +(+(s(x4211),x4212),+(s(x688),x690)) +(s(x4214),+(x4215,s(x704))) <-17|[]- +(+(s(x4214),x4215),s(x704)) -8| []-> s(+(+(s(x4214),x4215),x704)) +(s(x844),+(x845,s(x4219))) <-17|[]- +(+(s(x844),x845),s(x4219)) -11| []-> +(s(x844),+(x845,s(x4219))) +(x870,+(s(x4220),+(x4221,s(x872)))) <-17|1[]- +(x870,+(+(s(x4220),x4221),s(x872))) -12| []-> +(+(x870,+(s(x4220),x4221)),s(x872)) +(s(x4223),+(x921,s(x922))) <-17|[]- +(+(s(x4223),x921),s(x922)) -13| []-> +(s(x4223),+(x921,s(x922))) +(+(s(x4226),+(x4227,s(x4228))),s(x922)) <-17|0[]- +(+(+(s(x4226),x4227),s(x4228)),s(x922)) -13| []-> +(+(s(x4226),x4227), +(s(x4228),s(x922))) +(s(x963),+(s(x964),s(x4231))) <-17|[]- +(+(s(x963),s(x964)),s(x4231)) -15| []-> +(s(x963),+(s(x964),s(x4231))) Redundant Rules Transformation: +(x649,0()) -> x649 +(x675,+(x676,x678)) -> +(+(x675,x676),x678) +(x702,s(x704)) -> s(+(x702,x704)) Church Rosser Transformation Processor (ac): +(x649,0()) -> x649 +(x675,+(x676,x678)) -> +(+(x675,x676),x678) +(x702,s(x704)) -> s(+(x702,x704)) AC critical peaks: joinable AC-KBO Processor: precedence: + > s ~ 0 weight function: [+](x0, x1) = x0 + 2x1 + 1, [0] = 2, [s](x0) = x0 + 2 problem: Qed