%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Tue May 5 06:56:49 PM UTC 2026
% Result : Theorem 0.75s 1.28s
% Output : Refutation 0.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n019.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % DateTime : Tue May 5 12:14:14 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.75/1.28 *** allocated 10000 integers for termspace/termends
% 0.75/1.28 *** allocated 10000 integers for clauses
% 0.75/1.28 *** allocated 10000 integers for justifications
% 0.75/1.28 Bliksem 1.12
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28 Automatic Strategy Selection
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28 Clauses:
% 0.75/1.28
% 0.75/1.28 { head( cons( X, Y ) ) = X }.
% 0.75/1.28 { tail( cons( X, Y ) ) = Y }.
% 0.75/1.28 { ! nil = cons( X, Y ) }.
% 0.75/1.28 { proj1Suc( suc( X ) ) = X }.
% 0.75/1.28 { ! zero = suc( X ) }.
% 0.75/1.28 { ! i = o }.
% 0.75/1.28 { half( zero ) = zero }.
% 0.75/1.28 { half( suc( zero ) ) = zero }.
% 0.75/1.28 { half( suc( suc( X ) ) ) = suc( half( X ) ) }.
% 0.75/1.28 { evenNat( zero ) }.
% 0.75/1.28 { ! evenNat( suc( X ) ), ! evenNat( X ) }.
% 0.75/1.28 { evenNat( X ), evenNat( suc( X ) ) }.
% 0.75/1.28 { shw( zero ) = nil }.
% 0.75/1.28 { ! evenNat( suc( X ) ), shw( suc( X ) ) = cons( o, shw( half( suc( X ) ) )
% 0.75/1.28 ) }.
% 0.75/1.28 { evenNat( suc( X ) ), shw( suc( X ) ) = cons( i, shw( half( suc( X ) ) ) )
% 0.75/1.28 }.
% 0.75/1.28 { append( nil, X ) = X }.
% 0.75/1.28 { append( cons( Y, Z ), X ) = cons( Y, append( Z, X ) ) }.
% 0.75/1.28 { addNat( zero, X ) = X }.
% 0.75/1.28 { addNat( suc( Y ), X ) = suc( addNat( Y, X ) ) }.
% 0.75/1.28 { double( X ) = addNat( X, X ) }.
% 0.75/1.28 { rd( nil ) = zero }.
% 0.75/1.28 { rd( cons( i, X ) ) = suc( double( rd( X ) ) ) }.
% 0.75/1.28 { rd( cons( o, X ) ) = double( rd( X ) ) }.
% 0.75/1.28 { x( X, Y ) = rd( append( shw( X ), shw( Y ) ) ) }.
% 0.75/1.28 { x( X, Y ) = x( Y, X ) }.
% 0.75/1.28
% 0.75/1.28 percentage equality = 0.758621, percentage horn = 0.920000
% 0.75/1.28 This is a problem with some equality
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28 Options Used:
% 0.75/1.28
% 0.75/1.28 useres = 1
% 0.75/1.28 useparamod = 1
% 0.75/1.28 useeqrefl = 1
% 0.75/1.28 useeqfact = 1
% 0.75/1.28 usefactor = 1
% 0.75/1.28 usesimpsplitting = 0
% 0.75/1.28 usesimpdemod = 5
% 0.75/1.28 usesimpres = 3
% 0.75/1.28
% 0.75/1.28 resimpinuse = 1000
% 0.75/1.28 resimpclauses = 20000
% 0.75/1.28 substype = eqrewr
% 0.75/1.28 backwardsubs = 1
% 0.75/1.28 selectoldest = 5
% 0.75/1.28
% 0.75/1.28 litorderings [0] = split
% 0.75/1.28 litorderings [1] = extend the termordering, first sorting on arguments
% 0.75/1.28
% 0.75/1.28 termordering = kbo
% 0.75/1.28
% 0.75/1.28 litapriori = 0
% 0.75/1.28 termapriori = 1
% 0.75/1.28 litaposteriori = 0
% 0.75/1.28 termaposteriori = 0
% 0.75/1.28 demodaposteriori = 0
% 0.75/1.28 ordereqreflfact = 0
% 0.75/1.28
% 0.75/1.28 litselect = negord
% 0.75/1.28
% 0.75/1.28 maxweight = 15
% 0.75/1.28 maxdepth = 30000
% 0.75/1.28 maxlength = 115
% 0.75/1.28 maxnrvars = 195
% 0.75/1.28 excuselevel = 1
% 0.75/1.28 increasemaxweight = 1
% 0.75/1.28
% 0.75/1.28 maxselected = 10000000
% 0.75/1.28 maxnrclauses = 10000000
% 0.75/1.28
% 0.75/1.28 showgenerated = 0
% 0.75/1.28 showkept = 0
% 0.75/1.28 showselected = 0
% 0.75/1.28 showdeleted = 0
% 0.75/1.28 showresimp = 1
% 0.75/1.28 showstatus = 2000
% 0.75/1.28
% 0.75/1.28 prologoutput = 0
% 0.75/1.28 nrgoals = 5000000
% 0.75/1.28 totalproof = 1
% 0.75/1.28
% 0.75/1.28 Symbols occurring in the translation:
% 0.75/1.28
% 0.75/1.28 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.75/1.28 . [1, 2] (w:1, o:30, a:1, s:1, b:0),
% 0.75/1.28 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.75/1.28 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.75/1.28 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.75/1.28 cons [37, 2] (w:1, o:54, a:1, s:1, b:0),
% 0.75/1.28 head [38, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.75/1.28 tail [39, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.75/1.28 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.75/1.28 suc [41, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.75/1.28 proj1Suc [42, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.75/1.28 zero [43, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.75/1.28 i [44, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.75/1.28 o [45, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.75/1.28 half [46, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.75/1.28 evenNat [48, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.75/1.28 shw [49, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.75/1.28 append [51, 2] (w:1, o:55, a:1, s:1, b:0),
% 0.75/1.28 addNat [54, 2] (w:1, o:56, a:1, s:1, b:0),
% 0.75/1.28 double [55, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.75/1.28 rd [56, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.75/1.28 x [57, 2] (w:1, o:57, a:1, s:1, b:0).
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28 Starting Search:
% 0.75/1.28
% 0.75/1.28 *** allocated 15000 integers for clauses
% 0.75/1.28 *** allocated 22500 integers for clauses
% 0.75/1.28 *** allocated 33750 integers for clauses
% 0.75/1.28 *** allocated 50625 integers for clauses
% 0.75/1.28 *** allocated 15000 integers for termspace/termends
% 0.75/1.28 *** allocated 75937 integers for clauses
% 0.75/1.28 Resimplifying inuse:
% 0.75/1.28 Done
% 0.75/1.28
% 0.75/1.28 *** allocated 22500 integers for termspace/termends
% 0.75/1.28 *** allocated 113905 integers for clauses
% 0.75/1.28 *** allocated 33750 integers for termspace/termends
% 0.75/1.28 *** allocated 170857 integers for clauses
% 0.75/1.28
% 0.75/1.28 Intermediate Status:
% 0.75/1.28 Generated: 14428
% 0.75/1.28 Kept: 2014
% 0.75/1.28 Inuse: 411
% 0.75/1.28 Deleted: 42
% 0.75/1.28 Deletedinuse: 10
% 0.75/1.28
% 0.75/1.28 Resimplifying inuse:
% 0.75/1.28 Done
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28 Bliksems!, er is een bewijs:
% 0.75/1.28 % SZS status Theorem
% 0.75/1.28 % SZS output start Refutation
% 0.75/1.28
% 0.75/1.28 (3) {G0,W5,D4,L1,V1,M1} I { proj1Suc( suc( X ) ) ==> X }.
% 0.75/1.28 (6) {G0,W4,D3,L1,V0,M1} I { half( zero ) ==> zero }.
% 0.75/1.28 (7) {G0,W5,D4,L1,V0,M1} I { half( suc( zero ) ) ==> zero }.
% 0.75/1.28 (8) {G0,W8,D5,L1,V1,M1} I { half( suc( suc( X ) ) ) ==> suc( half( X ) )
% 0.75/1.28 }.
% 0.75/1.28 (9) {G0,W2,D2,L1,V0,M1} I { evenNat( zero ) }.
% 0.75/1.28 (10) {G0,W5,D3,L2,V1,M2} I { ! evenNat( suc( X ) ), ! evenNat( X ) }.
% 0.75/1.28 (11) {G0,W5,D3,L2,V1,M2} I { evenNat( X ), evenNat( suc( X ) ) }.
% 0.75/1.28 (12) {G0,W4,D3,L1,V0,M1} I { shw( zero ) ==> nil }.
% 0.75/1.28 (13) {G0,W13,D6,L2,V1,M2} I { ! evenNat( suc( X ) ), cons( o, shw( half(
% 0.75/1.28 suc( X ) ) ) ) ==> shw( suc( X ) ) }.
% 0.75/1.28 (14) {G0,W13,D6,L2,V1,M2} I { evenNat( suc( X ) ), cons( i, shw( half( suc
% 0.75/1.28 ( X ) ) ) ) ==> shw( suc( X ) ) }.
% 0.75/1.28 (15) {G0,W5,D3,L1,V1,M1} I { append( nil, X ) ==> X }.
% 0.75/1.28 (16) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==> cons( Y, append
% 0.75/1.28 ( Z, X ) ) }.
% 0.75/1.28 (17) {G0,W5,D3,L1,V1,M1} I { addNat( zero, X ) ==> X }.
% 0.75/1.28 (18) {G0,W9,D4,L1,V2,M1} I { addNat( suc( Y ), X ) ==> suc( addNat( Y, X )
% 0.75/1.28 ) }.
% 0.75/1.28 (19) {G0,W6,D3,L1,V1,M1} I { addNat( X, X ) ==> double( X ) }.
% 0.75/1.28 (20) {G0,W4,D3,L1,V0,M1} I { rd( nil ) ==> zero }.
% 0.75/1.28 (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd( cons( i, X )
% 0.75/1.28 ) }.
% 0.75/1.28 (22) {G0,W8,D4,L1,V1,M1} I { rd( cons( o, X ) ) ==> double( rd( X ) ) }.
% 0.75/1.28 (23) {G0,W10,D5,L1,V2,M1} I { rd( append( shw( X ), shw( Y ) ) ) ==> x( X,
% 0.75/1.28 Y ) }.
% 0.75/1.28 (24) {G0,W7,D3,L1,V2,M1} I { x( X, Y ) = x( Y, X ) }.
% 0.75/1.28 (27) {G1,W3,D3,L1,V0,M1} R(10,9) { ! evenNat( suc( zero ) ) }.
% 0.75/1.28 (28) {G2,W4,D4,L1,V0,M1} R(27,11) { evenNat( suc( suc( zero ) ) ) }.
% 0.75/1.28 (29) {G3,W5,D5,L1,V0,M1} R(28,10) { ! evenNat( suc( suc( suc( zero ) ) ) )
% 0.75/1.28 }.
% 0.75/1.28 (31) {G1,W4,D3,L1,V0,M1} P(19,17) { double( zero ) ==> zero }.
% 0.75/1.28 (41) {G3,W10,D5,L1,V0,M1} R(13,28);d(8);d(6) { cons( o, shw( suc( zero ) )
% 0.75/1.28 ) ==> shw( suc( suc( zero ) ) ) }.
% 0.75/1.28 (61) {G4,W11,D6,L1,V0,M1} R(14,29);d(8);d(7) { cons( i, shw( suc( zero ) )
% 0.75/1.28 ) ==> shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 (62) {G2,W7,D4,L1,V0,M1} R(14,27);d(7);d(12) { cons( i, nil ) ==> shw( suc
% 0.75/1.28 ( zero ) ) }.
% 0.75/1.28 (70) {G3,W9,D5,L1,V1,M1} P(62,16);d(15) { append( shw( suc( zero ) ), X )
% 0.75/1.28 ==> cons( i, X ) }.
% 0.75/1.28 (79) {G1,W9,D5,L1,V1,M1} P(18,19) { suc( addNat( X, suc( X ) ) ) ==> double
% 0.75/1.28 ( suc( X ) ) }.
% 0.75/1.28 (93) {G1,W9,D4,L2,V1,M2} P(21,10) { ! evenNat( rd( cons( i, X ) ) ), !
% 0.75/1.28 evenNat( double( rd( X ) ) ) }.
% 0.75/1.28 (95) {G3,W7,D5,L1,V0,M1} P(20,21);d(31);d(62) { rd( shw( suc( zero ) ) )
% 0.75/1.28 ==> suc( zero ) }.
% 0.75/1.28 (99) {G5,W11,D7,L1,V0,M1} P(95,21);d(61) { rd( shw( suc( suc( suc( zero ) )
% 0.75/1.28 ) ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 (128) {G2,W9,D5,L1,V1,M1} P(79,3) { proj1Suc( double( suc( X ) ) ) = addNat
% 0.75/1.28 ( X, suc( X ) ) }.
% 0.75/1.28 (130) {G2,W9,D4,L2,V1,M2} P(79,11) { evenNat( addNat( X, suc( X ) ) ),
% 0.75/1.28 evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 (131) {G2,W7,D4,L1,V0,M1} P(17,79) { double( suc( zero ) ) ==> suc( suc(
% 0.75/1.28 zero ) ) }.
% 0.75/1.28 (150) {G4,W12,D6,L1,V1,M1} P(41,16);d(70) { append( shw( suc( suc( zero ) )
% 0.75/1.28 ), X ) ==> cons( o, cons( i, X ) ) }.
% 0.75/1.28 (151) {G4,W9,D6,L1,V0,M1} P(41,22);d(95);d(131) { rd( shw( suc( suc( zero )
% 0.75/1.28 ) ) ) ==> suc( suc( zero ) ) }.
% 0.75/1.28 (167) {G3,W9,D5,L2,V1,M2} P(128,130) { evenNat( proj1Suc( double( suc( X )
% 0.75/1.28 ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 (169) {G3,W9,D6,L1,V1,M1} P(128,79) { suc( proj1Suc( double( suc( X ) ) ) )
% 0.75/1.28 ==> double( suc( X ) ) }.
% 0.75/1.28 (170) {G3,W14,D6,L1,V1,M1} P(79,128) { addNat( addNat( X, suc( X ) ),
% 0.75/1.28 double( suc( X ) ) ) ==> proj1Suc( double( double( suc( X ) ) ) ) }.
% 0.75/1.28 (171) {G3,W15,D6,L1,V1,M1} P(21,128) { addNat( double( rd( X ) ), rd( cons
% 0.75/1.28 ( i, X ) ) ) ==> proj1Suc( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 (173) {G4,W10,D5,L1,V1,M1} P(70,23) { rd( cons( i, shw( X ) ) ) ==> x( suc
% 0.75/1.28 ( zero ), X ) }.
% 0.75/1.28 (193) {G4,W10,D5,L2,V1,M2} R(167,10) { evenNat( proj1Suc( double( suc( X )
% 0.75/1.28 ) ) ), ! evenNat( suc( double( suc( X ) ) ) ) }.
% 0.75/1.28 (195) {G4,W13,D6,L2,V1,M2} P(21,167) { evenNat( proj1Suc( double( rd( cons
% 0.75/1.28 ( i, X ) ) ) ) ), evenNat( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 (320) {G5,W10,D5,L2,V1,M2} P(173,93) { ! evenNat( x( suc( zero ), X ) ), !
% 0.75/1.28 evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 (395) {G6,W10,D5,L2,V1,M2} P(24,320) { ! evenNat( x( X, suc( zero ) ) ), !
% 0.75/1.28 evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 (489) {G6,W10,D5,L1,V0,M1} P(61,173);d(99);d(131) { x( suc( zero ), suc(
% 0.75/1.28 zero ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 (1072) {G6,W11,D7,L1,V0,M1} S(99);d(131) { rd( shw( suc( suc( suc( zero ) )
% 0.75/1.28 ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 (1478) {G5,W11,D5,L1,V1,M1} P(150,23);d(22);d(173) { x( suc( suc( zero ) )
% 0.75/1.28 , X ) ==> double( x( suc( zero ), X ) ) }.
% 0.75/1.28 (1712) {G4,W10,D6,L1,V0,M1} P(17,170);d(18);d(17);d(131) { proj1Suc( double
% 0.75/1.28 ( suc( suc( zero ) ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 (1714) {G5,W6,D6,L1,V0,M1} P(1712,193);r(29) { ! evenNat( suc( double( suc
% 0.75/1.28 ( suc( zero ) ) ) ) ) }.
% 0.75/1.28 (1715) {G5,W10,D6,L1,V0,M1} P(1712,169) { suc( suc( suc( suc( zero ) ) ) )
% 0.75/1.28 ==> double( suc( suc( zero ) ) ) }.
% 0.75/1.28 (1716) {G5,W5,D5,L1,V0,M1} P(1712,167);r(29) { evenNat( double( suc( suc(
% 0.75/1.28 zero ) ) ) ) }.
% 0.75/1.28 (1767) {G7,W12,D7,L1,V0,M1} P(61,171);d(95);d(131);d(18);d(18);d(17);d(1072
% 0.75/1.28 );d(1715) { proj1Suc( double( suc( suc( suc( zero ) ) ) ) ) ==> suc(
% 0.75/1.28 double( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 (2142) {G8,W6,D6,L1,V0,M1} P(61,195);d(1072);d(1072);d(1767);r(1714) {
% 0.75/1.28 evenNat( double( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.28 (2284) {G9,W5,D5,L1,V0,M1} P(1478,395);d(489);d(151);r(2142) { ! evenNat(
% 0.75/1.28 double( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 (2287) {G10,W0,D0,L0,V0,M0} S(2284);r(1716) { }.
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28 % SZS output end Refutation
% 0.75/1.28 found a proof!
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28 Unprocessed initial clauses:
% 0.75/1.28
% 0.75/1.28 (2289) {G0,W6,D4,L1,V2,M1} { head( cons( X, Y ) ) = X }.
% 0.75/1.28 (2290) {G0,W6,D4,L1,V2,M1} { tail( cons( X, Y ) ) = Y }.
% 0.75/1.28 (2291) {G0,W5,D3,L1,V2,M1} { ! nil = cons( X, Y ) }.
% 0.75/1.28 (2292) {G0,W5,D4,L1,V1,M1} { proj1Suc( suc( X ) ) = X }.
% 0.75/1.28 (2293) {G0,W4,D3,L1,V1,M1} { ! zero = suc( X ) }.
% 0.75/1.28 (2294) {G0,W3,D2,L1,V0,M1} { ! i = o }.
% 0.75/1.28 (2295) {G0,W4,D3,L1,V0,M1} { half( zero ) = zero }.
% 0.75/1.28 (2296) {G0,W5,D4,L1,V0,M1} { half( suc( zero ) ) = zero }.
% 0.75/1.28 (2297) {G0,W8,D5,L1,V1,M1} { half( suc( suc( X ) ) ) = suc( half( X ) )
% 0.75/1.28 }.
% 0.75/1.28 (2298) {G0,W2,D2,L1,V0,M1} { evenNat( zero ) }.
% 0.75/1.28 (2299) {G0,W5,D3,L2,V1,M2} { ! evenNat( suc( X ) ), ! evenNat( X ) }.
% 0.75/1.28 (2300) {G0,W5,D3,L2,V1,M2} { evenNat( X ), evenNat( suc( X ) ) }.
% 0.75/1.28 (2301) {G0,W4,D3,L1,V0,M1} { shw( zero ) = nil }.
% 0.75/1.28 (2302) {G0,W13,D6,L2,V1,M2} { ! evenNat( suc( X ) ), shw( suc( X ) ) =
% 0.75/1.28 cons( o, shw( half( suc( X ) ) ) ) }.
% 0.75/1.28 (2303) {G0,W13,D6,L2,V1,M2} { evenNat( suc( X ) ), shw( suc( X ) ) = cons
% 0.75/1.28 ( i, shw( half( suc( X ) ) ) ) }.
% 0.75/1.28 (2304) {G0,W5,D3,L1,V1,M1} { append( nil, X ) = X }.
% 0.75/1.28 (2305) {G0,W11,D4,L1,V3,M1} { append( cons( Y, Z ), X ) = cons( Y, append
% 0.75/1.28 ( Z, X ) ) }.
% 0.75/1.28 (2306) {G0,W5,D3,L1,V1,M1} { addNat( zero, X ) = X }.
% 0.75/1.28 (2307) {G0,W9,D4,L1,V2,M1} { addNat( suc( Y ), X ) = suc( addNat( Y, X ) )
% 0.75/1.28 }.
% 0.75/1.28 (2308) {G0,W6,D3,L1,V1,M1} { double( X ) = addNat( X, X ) }.
% 0.75/1.28 (2309) {G0,W4,D3,L1,V0,M1} { rd( nil ) = zero }.
% 0.75/1.28 (2310) {G0,W9,D5,L1,V1,M1} { rd( cons( i, X ) ) = suc( double( rd( X ) ) )
% 0.75/1.28 }.
% 0.75/1.28 (2311) {G0,W8,D4,L1,V1,M1} { rd( cons( o, X ) ) = double( rd( X ) ) }.
% 0.75/1.28 (2312) {G0,W10,D5,L1,V2,M1} { x( X, Y ) = rd( append( shw( X ), shw( Y ) )
% 0.75/1.28 ) }.
% 0.75/1.28 (2313) {G0,W7,D3,L1,V2,M1} { x( X, Y ) = x( Y, X ) }.
% 0.75/1.28
% 0.75/1.28
% 0.75/1.28 Total Proof:
% 0.75/1.28
% 0.75/1.28 subsumption: (3) {G0,W5,D4,L1,V1,M1} I { proj1Suc( suc( X ) ) ==> X }.
% 0.75/1.28 parent0: (2292) {G0,W5,D4,L1,V1,M1} { proj1Suc( suc( X ) ) = X }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (6) {G0,W4,D3,L1,V0,M1} I { half( zero ) ==> zero }.
% 0.75/1.28 parent0: (2295) {G0,W4,D3,L1,V0,M1} { half( zero ) = zero }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (7) {G0,W5,D4,L1,V0,M1} I { half( suc( zero ) ) ==> zero }.
% 0.75/1.28 parent0: (2296) {G0,W5,D4,L1,V0,M1} { half( suc( zero ) ) = zero }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (8) {G0,W8,D5,L1,V1,M1} I { half( suc( suc( X ) ) ) ==> suc(
% 0.75/1.28 half( X ) ) }.
% 0.75/1.28 parent0: (2297) {G0,W8,D5,L1,V1,M1} { half( suc( suc( X ) ) ) = suc( half
% 0.75/1.28 ( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (9) {G0,W2,D2,L1,V0,M1} I { evenNat( zero ) }.
% 0.75/1.28 parent0: (2298) {G0,W2,D2,L1,V0,M1} { evenNat( zero ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (10) {G0,W5,D3,L2,V1,M2} I { ! evenNat( suc( X ) ), ! evenNat
% 0.75/1.28 ( X ) }.
% 0.75/1.28 parent0: (2299) {G0,W5,D3,L2,V1,M2} { ! evenNat( suc( X ) ), ! evenNat( X
% 0.75/1.28 ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 1 ==> 1
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (11) {G0,W5,D3,L2,V1,M2} I { evenNat( X ), evenNat( suc( X ) )
% 0.75/1.28 }.
% 0.75/1.28 parent0: (2300) {G0,W5,D3,L2,V1,M2} { evenNat( X ), evenNat( suc( X ) )
% 0.75/1.28 }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 1 ==> 1
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (12) {G0,W4,D3,L1,V0,M1} I { shw( zero ) ==> nil }.
% 0.75/1.28 parent0: (2301) {G0,W4,D3,L1,V0,M1} { shw( zero ) = nil }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2389) {G0,W13,D6,L2,V1,M2} { cons( o, shw( half( suc( X ) ) ) ) =
% 0.75/1.28 shw( suc( X ) ), ! evenNat( suc( X ) ) }.
% 0.75/1.28 parent0[1]: (2302) {G0,W13,D6,L2,V1,M2} { ! evenNat( suc( X ) ), shw( suc
% 0.75/1.28 ( X ) ) = cons( o, shw( half( suc( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (13) {G0,W13,D6,L2,V1,M2} I { ! evenNat( suc( X ) ), cons( o,
% 0.75/1.28 shw( half( suc( X ) ) ) ) ==> shw( suc( X ) ) }.
% 0.75/1.28 parent0: (2389) {G0,W13,D6,L2,V1,M2} { cons( o, shw( half( suc( X ) ) ) )
% 0.75/1.28 = shw( suc( X ) ), ! evenNat( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 1
% 0.75/1.28 1 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2401) {G0,W13,D6,L2,V1,M2} { cons( i, shw( half( suc( X ) ) ) ) =
% 0.75/1.28 shw( suc( X ) ), evenNat( suc( X ) ) }.
% 0.75/1.28 parent0[1]: (2303) {G0,W13,D6,L2,V1,M2} { evenNat( suc( X ) ), shw( suc( X
% 0.75/1.28 ) ) = cons( i, shw( half( suc( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (14) {G0,W13,D6,L2,V1,M2} I { evenNat( suc( X ) ), cons( i,
% 0.75/1.28 shw( half( suc( X ) ) ) ) ==> shw( suc( X ) ) }.
% 0.75/1.28 parent0: (2401) {G0,W13,D6,L2,V1,M2} { cons( i, shw( half( suc( X ) ) ) )
% 0.75/1.28 = shw( suc( X ) ), evenNat( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 1
% 0.75/1.28 1 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (15) {G0,W5,D3,L1,V1,M1} I { append( nil, X ) ==> X }.
% 0.75/1.28 parent0: (2304) {G0,W5,D3,L1,V1,M1} { append( nil, X ) = X }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (16) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==>
% 0.75/1.28 cons( Y, append( Z, X ) ) }.
% 0.75/1.28 parent0: (2305) {G0,W11,D4,L1,V3,M1} { append( cons( Y, Z ), X ) = cons( Y
% 0.75/1.28 , append( Z, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 Y := Y
% 0.75/1.28 Z := Z
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (17) {G0,W5,D3,L1,V1,M1} I { addNat( zero, X ) ==> X }.
% 0.75/1.28 parent0: (2306) {G0,W5,D3,L1,V1,M1} { addNat( zero, X ) = X }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (18) {G0,W9,D4,L1,V2,M1} I { addNat( suc( Y ), X ) ==> suc(
% 0.75/1.28 addNat( Y, X ) ) }.
% 0.75/1.28 parent0: (2307) {G0,W9,D4,L1,V2,M1} { addNat( suc( Y ), X ) = suc( addNat
% 0.75/1.28 ( Y, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 Y := Y
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2476) {G0,W6,D3,L1,V1,M1} { addNat( X, X ) = double( X ) }.
% 0.75/1.28 parent0[0]: (2308) {G0,W6,D3,L1,V1,M1} { double( X ) = addNat( X, X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (19) {G0,W6,D3,L1,V1,M1} I { addNat( X, X ) ==> double( X )
% 0.75/1.28 }.
% 0.75/1.28 parent0: (2476) {G0,W6,D3,L1,V1,M1} { addNat( X, X ) = double( X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (20) {G0,W4,D3,L1,V0,M1} I { rd( nil ) ==> zero }.
% 0.75/1.28 parent0: (2309) {G0,W4,D3,L1,V0,M1} { rd( nil ) = zero }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2513) {G0,W9,D5,L1,V1,M1} { suc( double( rd( X ) ) ) = rd( cons(
% 0.75/1.28 i, X ) ) }.
% 0.75/1.28 parent0[0]: (2310) {G0,W9,D5,L1,V1,M1} { rd( cons( i, X ) ) = suc( double
% 0.75/1.28 ( rd( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd(
% 0.75/1.28 cons( i, X ) ) }.
% 0.75/1.28 parent0: (2513) {G0,W9,D5,L1,V1,M1} { suc( double( rd( X ) ) ) = rd( cons
% 0.75/1.28 ( i, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (22) {G0,W8,D4,L1,V1,M1} I { rd( cons( o, X ) ) ==> double( rd
% 0.75/1.28 ( X ) ) }.
% 0.75/1.28 parent0: (2311) {G0,W8,D4,L1,V1,M1} { rd( cons( o, X ) ) = double( rd( X )
% 0.75/1.28 ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2554) {G0,W10,D5,L1,V2,M1} { rd( append( shw( X ), shw( Y ) ) ) =
% 0.75/1.28 x( X, Y ) }.
% 0.75/1.28 parent0[0]: (2312) {G0,W10,D5,L1,V2,M1} { x( X, Y ) = rd( append( shw( X )
% 0.75/1.28 , shw( Y ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 Y := Y
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (23) {G0,W10,D5,L1,V2,M1} I { rd( append( shw( X ), shw( Y ) )
% 0.75/1.28 ) ==> x( X, Y ) }.
% 0.75/1.28 parent0: (2554) {G0,W10,D5,L1,V2,M1} { rd( append( shw( X ), shw( Y ) ) )
% 0.75/1.28 = x( X, Y ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 Y := Y
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (24) {G0,W7,D3,L1,V2,M1} I { x( X, Y ) = x( Y, X ) }.
% 0.75/1.28 parent0: (2313) {G0,W7,D3,L1,V2,M1} { x( X, Y ) = x( Y, X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 Y := Y
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 resolution: (2576) {G1,W3,D3,L1,V0,M1} { ! evenNat( suc( zero ) ) }.
% 0.75/1.28 parent0[1]: (10) {G0,W5,D3,L2,V1,M2} I { ! evenNat( suc( X ) ), ! evenNat(
% 0.75/1.28 X ) }.
% 0.75/1.28 parent1[0]: (9) {G0,W2,D2,L1,V0,M1} I { evenNat( zero ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := zero
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (27) {G1,W3,D3,L1,V0,M1} R(10,9) { ! evenNat( suc( zero ) )
% 0.75/1.28 }.
% 0.75/1.28 parent0: (2576) {G1,W3,D3,L1,V0,M1} { ! evenNat( suc( zero ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 resolution: (2577) {G1,W4,D4,L1,V0,M1} { evenNat( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (27) {G1,W3,D3,L1,V0,M1} R(10,9) { ! evenNat( suc( zero ) ) }.
% 0.75/1.28 parent1[0]: (11) {G0,W5,D3,L2,V1,M2} I { evenNat( X ), evenNat( suc( X ) )
% 0.75/1.28 }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := suc( zero )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (28) {G2,W4,D4,L1,V0,M1} R(27,11) { evenNat( suc( suc( zero )
% 0.75/1.28 ) ) }.
% 0.75/1.28 parent0: (2577) {G1,W4,D4,L1,V0,M1} { evenNat( suc( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 resolution: (2580) {G1,W5,D5,L1,V0,M1} { ! evenNat( suc( suc( suc( zero )
% 0.75/1.28 ) ) ) }.
% 0.75/1.28 parent0[1]: (10) {G0,W5,D3,L2,V1,M2} I { ! evenNat( suc( X ) ), ! evenNat(
% 0.75/1.28 X ) }.
% 0.75/1.28 parent1[0]: (28) {G2,W4,D4,L1,V0,M1} R(27,11) { evenNat( suc( suc( zero ) )
% 0.75/1.28 ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := suc( suc( zero ) )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (29) {G3,W5,D5,L1,V0,M1} R(28,10) { ! evenNat( suc( suc( suc(
% 0.75/1.28 zero ) ) ) ) }.
% 0.75/1.28 parent0: (2580) {G1,W5,D5,L1,V0,M1} { ! evenNat( suc( suc( suc( zero ) ) )
% 0.75/1.28 ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2581) {G0,W6,D3,L1,V1,M1} { double( X ) ==> addNat( X, X ) }.
% 0.75/1.28 parent0[0]: (19) {G0,W6,D3,L1,V1,M1} I { addNat( X, X ) ==> double( X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2583) {G1,W4,D3,L1,V0,M1} { double( zero ) ==> zero }.
% 0.75/1.28 parent0[0]: (17) {G0,W5,D3,L1,V1,M1} I { addNat( zero, X ) ==> X }.
% 0.75/1.28 parent1[0; 3]: (2581) {G0,W6,D3,L1,V1,M1} { double( X ) ==> addNat( X, X )
% 0.75/1.28 }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := zero
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := zero
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (31) {G1,W4,D3,L1,V0,M1} P(19,17) { double( zero ) ==> zero
% 0.75/1.28 }.
% 0.75/1.28 parent0: (2583) {G1,W4,D3,L1,V0,M1} { double( zero ) ==> zero }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2585) {G0,W13,D6,L2,V1,M2} { shw( suc( X ) ) ==> cons( o, shw(
% 0.75/1.28 half( suc( X ) ) ) ), ! evenNat( suc( X ) ) }.
% 0.75/1.28 parent0[1]: (13) {G0,W13,D6,L2,V1,M2} I { ! evenNat( suc( X ) ), cons( o,
% 0.75/1.28 shw( half( suc( X ) ) ) ) ==> shw( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 resolution: (2588) {G1,W12,D7,L1,V0,M1} { shw( suc( suc( zero ) ) ) ==>
% 0.75/1.28 cons( o, shw( half( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.28 parent0[1]: (2585) {G0,W13,D6,L2,V1,M2} { shw( suc( X ) ) ==> cons( o, shw
% 0.75/1.28 ( half( suc( X ) ) ) ), ! evenNat( suc( X ) ) }.
% 0.75/1.28 parent1[0]: (28) {G2,W4,D4,L1,V0,M1} R(27,11) { evenNat( suc( suc( zero ) )
% 0.75/1.28 ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := suc( zero )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2589) {G1,W11,D6,L1,V0,M1} { shw( suc( suc( zero ) ) ) ==> cons
% 0.75/1.28 ( o, shw( suc( half( zero ) ) ) ) }.
% 0.75/1.28 parent0[0]: (8) {G0,W8,D5,L1,V1,M1} I { half( suc( suc( X ) ) ) ==> suc(
% 0.75/1.28 half( X ) ) }.
% 0.75/1.28 parent1[0; 8]: (2588) {G1,W12,D7,L1,V0,M1} { shw( suc( suc( zero ) ) ) ==>
% 0.75/1.28 cons( o, shw( half( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := zero
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2590) {G1,W10,D5,L1,V0,M1} { shw( suc( suc( zero ) ) ) ==> cons
% 0.75/1.28 ( o, shw( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (6) {G0,W4,D3,L1,V0,M1} I { half( zero ) ==> zero }.
% 0.75/1.28 parent1[0; 9]: (2589) {G1,W11,D6,L1,V0,M1} { shw( suc( suc( zero ) ) ) ==>
% 0.75/1.28 cons( o, shw( suc( half( zero ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2591) {G1,W10,D5,L1,V0,M1} { cons( o, shw( suc( zero ) ) ) ==>
% 0.75/1.28 shw( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (2590) {G1,W10,D5,L1,V0,M1} { shw( suc( suc( zero ) ) ) ==>
% 0.75/1.28 cons( o, shw( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (41) {G3,W10,D5,L1,V0,M1} R(13,28);d(8);d(6) { cons( o, shw(
% 0.75/1.28 suc( zero ) ) ) ==> shw( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0: (2591) {G1,W10,D5,L1,V0,M1} { cons( o, shw( suc( zero ) ) ) ==>
% 0.75/1.28 shw( suc( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 *** allocated 50625 integers for termspace/termends
% 0.75/1.28 eqswap: (2592) {G0,W13,D6,L2,V1,M2} { shw( suc( X ) ) ==> cons( i, shw(
% 0.75/1.28 half( suc( X ) ) ) ), evenNat( suc( X ) ) }.
% 0.75/1.28 parent0[1]: (14) {G0,W13,D6,L2,V1,M2} I { evenNat( suc( X ) ), cons( i, shw
% 0.75/1.28 ( half( suc( X ) ) ) ) ==> shw( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 resolution: (2595) {G1,W14,D8,L1,V0,M1} { shw( suc( suc( suc( zero ) ) ) )
% 0.75/1.28 ==> cons( i, shw( half( suc( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.28 parent0[0]: (29) {G3,W5,D5,L1,V0,M1} R(28,10) { ! evenNat( suc( suc( suc(
% 0.75/1.28 zero ) ) ) ) }.
% 0.75/1.28 parent1[1]: (2592) {G0,W13,D6,L2,V1,M2} { shw( suc( X ) ) ==> cons( i, shw
% 0.75/1.28 ( half( suc( X ) ) ) ), evenNat( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := suc( suc( zero ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2596) {G1,W13,D7,L1,V0,M1} { shw( suc( suc( suc( zero ) ) ) )
% 0.75/1.28 ==> cons( i, shw( suc( half( suc( zero ) ) ) ) ) }.
% 0.75/1.28 parent0[0]: (8) {G0,W8,D5,L1,V1,M1} I { half( suc( suc( X ) ) ) ==> suc(
% 0.75/1.28 half( X ) ) }.
% 0.75/1.28 parent1[0; 9]: (2595) {G1,W14,D8,L1,V0,M1} { shw( suc( suc( suc( zero ) )
% 0.75/1.28 ) ) ==> cons( i, shw( half( suc( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := suc( zero )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2597) {G1,W11,D6,L1,V0,M1} { shw( suc( suc( suc( zero ) ) ) )
% 0.75/1.28 ==> cons( i, shw( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (7) {G0,W5,D4,L1,V0,M1} I { half( suc( zero ) ) ==> zero }.
% 0.75/1.28 parent1[0; 10]: (2596) {G1,W13,D7,L1,V0,M1} { shw( suc( suc( suc( zero ) )
% 0.75/1.28 ) ) ==> cons( i, shw( suc( half( suc( zero ) ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2598) {G1,W11,D6,L1,V0,M1} { cons( i, shw( suc( zero ) ) ) ==>
% 0.75/1.28 shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 parent0[0]: (2597) {G1,W11,D6,L1,V0,M1} { shw( suc( suc( suc( zero ) ) ) )
% 0.75/1.28 ==> cons( i, shw( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (61) {G4,W11,D6,L1,V0,M1} R(14,29);d(8);d(7) { cons( i, shw(
% 0.75/1.28 suc( zero ) ) ) ==> shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 parent0: (2598) {G1,W11,D6,L1,V0,M1} { cons( i, shw( suc( zero ) ) ) ==>
% 0.75/1.28 shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2599) {G0,W13,D6,L2,V1,M2} { shw( suc( X ) ) ==> cons( i, shw(
% 0.75/1.28 half( suc( X ) ) ) ), evenNat( suc( X ) ) }.
% 0.75/1.28 parent0[1]: (14) {G0,W13,D6,L2,V1,M2} I { evenNat( suc( X ) ), cons( i, shw
% 0.75/1.28 ( half( suc( X ) ) ) ) ==> shw( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 resolution: (2602) {G1,W10,D6,L1,V0,M1} { shw( suc( zero ) ) ==> cons( i,
% 0.75/1.28 shw( half( suc( zero ) ) ) ) }.
% 0.75/1.28 parent0[0]: (27) {G1,W3,D3,L1,V0,M1} R(10,9) { ! evenNat( suc( zero ) ) }.
% 0.75/1.28 parent1[1]: (2599) {G0,W13,D6,L2,V1,M2} { shw( suc( X ) ) ==> cons( i, shw
% 0.75/1.28 ( half( suc( X ) ) ) ), evenNat( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := zero
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2603) {G1,W8,D4,L1,V0,M1} { shw( suc( zero ) ) ==> cons( i, shw
% 0.75/1.28 ( zero ) ) }.
% 0.75/1.28 parent0[0]: (7) {G0,W5,D4,L1,V0,M1} I { half( suc( zero ) ) ==> zero }.
% 0.75/1.28 parent1[0; 7]: (2602) {G1,W10,D6,L1,V0,M1} { shw( suc( zero ) ) ==> cons(
% 0.75/1.28 i, shw( half( suc( zero ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2604) {G1,W7,D4,L1,V0,M1} { shw( suc( zero ) ) ==> cons( i, nil
% 0.75/1.28 ) }.
% 0.75/1.28 parent0[0]: (12) {G0,W4,D3,L1,V0,M1} I { shw( zero ) ==> nil }.
% 0.75/1.28 parent1[0; 6]: (2603) {G1,W8,D4,L1,V0,M1} { shw( suc( zero ) ) ==> cons( i
% 0.75/1.28 , shw( zero ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2605) {G1,W7,D4,L1,V0,M1} { cons( i, nil ) ==> shw( suc( zero ) )
% 0.75/1.28 }.
% 0.75/1.28 parent0[0]: (2604) {G1,W7,D4,L1,V0,M1} { shw( suc( zero ) ) ==> cons( i,
% 0.75/1.28 nil ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (62) {G2,W7,D4,L1,V0,M1} R(14,27);d(7);d(12) { cons( i, nil )
% 0.75/1.28 ==> shw( suc( zero ) ) }.
% 0.75/1.28 parent0: (2605) {G1,W7,D4,L1,V0,M1} { cons( i, nil ) ==> shw( suc( zero )
% 0.75/1.28 ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2607) {G0,W11,D4,L1,V3,M1} { cons( X, append( Y, Z ) ) ==> append
% 0.75/1.28 ( cons( X, Y ), Z ) }.
% 0.75/1.28 parent0[0]: (16) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==>
% 0.75/1.28 cons( Y, append( Z, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := Z
% 0.75/1.28 Y := X
% 0.75/1.28 Z := Y
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2609) {G1,W11,D5,L1,V1,M1} { cons( i, append( nil, X ) ) ==>
% 0.75/1.28 append( shw( suc( zero ) ), X ) }.
% 0.75/1.28 parent0[0]: (62) {G2,W7,D4,L1,V0,M1} R(14,27);d(7);d(12) { cons( i, nil )
% 0.75/1.28 ==> shw( suc( zero ) ) }.
% 0.75/1.28 parent1[0; 7]: (2607) {G0,W11,D4,L1,V3,M1} { cons( X, append( Y, Z ) ) ==>
% 0.75/1.28 append( cons( X, Y ), Z ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := i
% 0.75/1.28 Y := nil
% 0.75/1.28 Z := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2610) {G1,W9,D5,L1,V1,M1} { cons( i, X ) ==> append( shw( suc(
% 0.75/1.28 zero ) ), X ) }.
% 0.75/1.28 parent0[0]: (15) {G0,W5,D3,L1,V1,M1} I { append( nil, X ) ==> X }.
% 0.75/1.28 parent1[0; 3]: (2609) {G1,W11,D5,L1,V1,M1} { cons( i, append( nil, X ) )
% 0.75/1.28 ==> append( shw( suc( zero ) ), X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2611) {G1,W9,D5,L1,V1,M1} { append( shw( suc( zero ) ), X ) ==>
% 0.75/1.28 cons( i, X ) }.
% 0.75/1.28 parent0[0]: (2610) {G1,W9,D5,L1,V1,M1} { cons( i, X ) ==> append( shw( suc
% 0.75/1.28 ( zero ) ), X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (70) {G3,W9,D5,L1,V1,M1} P(62,16);d(15) { append( shw( suc(
% 0.75/1.28 zero ) ), X ) ==> cons( i, X ) }.
% 0.75/1.28 parent0: (2611) {G1,W9,D5,L1,V1,M1} { append( shw( suc( zero ) ), X ) ==>
% 0.75/1.28 cons( i, X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2612) {G0,W9,D4,L1,V2,M1} { suc( addNat( X, Y ) ) ==> addNat( suc
% 0.75/1.28 ( X ), Y ) }.
% 0.75/1.28 parent0[0]: (18) {G0,W9,D4,L1,V2,M1} I { addNat( suc( Y ), X ) ==> suc(
% 0.75/1.28 addNat( Y, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := Y
% 0.75/1.28 Y := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2615) {G1,W9,D5,L1,V1,M1} { suc( addNat( X, suc( X ) ) ) ==>
% 0.75/1.28 double( suc( X ) ) }.
% 0.75/1.28 parent0[0]: (19) {G0,W6,D3,L1,V1,M1} I { addNat( X, X ) ==> double( X ) }.
% 0.75/1.28 parent1[0; 6]: (2612) {G0,W9,D4,L1,V2,M1} { suc( addNat( X, Y ) ) ==>
% 0.75/1.28 addNat( suc( X ), Y ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := suc( X )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 Y := suc( X )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (79) {G1,W9,D5,L1,V1,M1} P(18,19) { suc( addNat( X, suc( X ) )
% 0.75/1.28 ) ==> double( suc( X ) ) }.
% 0.75/1.28 parent0: (2615) {G1,W9,D5,L1,V1,M1} { suc( addNat( X, suc( X ) ) ) ==>
% 0.75/1.28 double( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2619) {G1,W9,D4,L2,V1,M2} { ! evenNat( rd( cons( i, X ) ) ), !
% 0.75/1.28 evenNat( double( rd( X ) ) ) }.
% 0.75/1.28 parent0[0]: (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd(
% 0.75/1.28 cons( i, X ) ) }.
% 0.75/1.28 parent1[0; 2]: (10) {G0,W5,D3,L2,V1,M2} I { ! evenNat( suc( X ) ), !
% 0.75/1.28 evenNat( X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := double( rd( X ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (93) {G1,W9,D4,L2,V1,M2} P(21,10) { ! evenNat( rd( cons( i, X
% 0.75/1.28 ) ) ), ! evenNat( double( rd( X ) ) ) }.
% 0.75/1.28 parent0: (2619) {G1,W9,D4,L2,V1,M2} { ! evenNat( rd( cons( i, X ) ) ), !
% 0.75/1.28 evenNat( double( rd( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 1 ==> 1
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2621) {G0,W9,D5,L1,V1,M1} { rd( cons( i, X ) ) ==> suc( double(
% 0.75/1.28 rd( X ) ) ) }.
% 0.75/1.28 parent0[0]: (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd(
% 0.75/1.28 cons( i, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2624) {G1,W8,D4,L1,V0,M1} { rd( cons( i, nil ) ) ==> suc( double
% 0.75/1.28 ( zero ) ) }.
% 0.75/1.28 parent0[0]: (20) {G0,W4,D3,L1,V0,M1} I { rd( nil ) ==> zero }.
% 0.75/1.28 parent1[0; 7]: (2621) {G0,W9,D5,L1,V1,M1} { rd( cons( i, X ) ) ==> suc(
% 0.75/1.28 double( rd( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := nil
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2625) {G2,W7,D4,L1,V0,M1} { rd( cons( i, nil ) ) ==> suc( zero )
% 0.75/1.28 }.
% 0.75/1.28 parent0[0]: (31) {G1,W4,D3,L1,V0,M1} P(19,17) { double( zero ) ==> zero }.
% 0.75/1.28 parent1[0; 6]: (2624) {G1,W8,D4,L1,V0,M1} { rd( cons( i, nil ) ) ==> suc(
% 0.75/1.28 double( zero ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2626) {G3,W7,D5,L1,V0,M1} { rd( shw( suc( zero ) ) ) ==> suc(
% 0.75/1.28 zero ) }.
% 0.75/1.28 parent0[0]: (62) {G2,W7,D4,L1,V0,M1} R(14,27);d(7);d(12) { cons( i, nil )
% 0.75/1.28 ==> shw( suc( zero ) ) }.
% 0.75/1.28 parent1[0; 2]: (2625) {G2,W7,D4,L1,V0,M1} { rd( cons( i, nil ) ) ==> suc(
% 0.75/1.28 zero ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (95) {G3,W7,D5,L1,V0,M1} P(20,21);d(31);d(62) { rd( shw( suc(
% 0.75/1.28 zero ) ) ) ==> suc( zero ) }.
% 0.75/1.28 parent0: (2626) {G3,W7,D5,L1,V0,M1} { rd( shw( suc( zero ) ) ) ==> suc(
% 0.75/1.28 zero ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2629) {G0,W9,D5,L1,V1,M1} { rd( cons( i, X ) ) ==> suc( double(
% 0.75/1.28 rd( X ) ) ) }.
% 0.75/1.28 parent0[0]: (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd(
% 0.75/1.28 cons( i, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2631) {G1,W11,D6,L1,V0,M1} { rd( cons( i, shw( suc( zero ) ) ) )
% 0.75/1.28 ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (95) {G3,W7,D5,L1,V0,M1} P(20,21);d(31);d(62) { rd( shw( suc(
% 0.75/1.28 zero ) ) ) ==> suc( zero ) }.
% 0.75/1.28 parent1[0; 9]: (2629) {G0,W9,D5,L1,V1,M1} { rd( cons( i, X ) ) ==> suc(
% 0.75/1.28 double( rd( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := shw( suc( zero ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2632) {G2,W11,D7,L1,V0,M1} { rd( shw( suc( suc( suc( zero ) ) )
% 0.75/1.28 ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (61) {G4,W11,D6,L1,V0,M1} R(14,29);d(8);d(7) { cons( i, shw(
% 0.75/1.28 suc( zero ) ) ) ==> shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 parent1[0; 2]: (2631) {G1,W11,D6,L1,V0,M1} { rd( cons( i, shw( suc( zero )
% 0.75/1.28 ) ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (99) {G5,W11,D7,L1,V0,M1} P(95,21);d(61) { rd( shw( suc( suc(
% 0.75/1.28 suc( zero ) ) ) ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 parent0: (2632) {G2,W11,D7,L1,V0,M1} { rd( shw( suc( suc( suc( zero ) ) )
% 0.75/1.28 ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2635) {G0,W5,D4,L1,V1,M1} { X ==> proj1Suc( suc( X ) ) }.
% 0.75/1.28 parent0[0]: (3) {G0,W5,D4,L1,V1,M1} I { proj1Suc( suc( X ) ) ==> X }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2636) {G1,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) ==> proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (79) {G1,W9,D5,L1,V1,M1} P(18,19) { suc( addNat( X, suc( X ) )
% 0.75/1.28 ) ==> double( suc( X ) ) }.
% 0.75/1.28 parent1[0; 6]: (2635) {G0,W5,D4,L1,V1,M1} { X ==> proj1Suc( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := addNat( X, suc( X ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2637) {G1,W9,D5,L1,V1,M1} { proj1Suc( double( suc( X ) ) ) ==>
% 0.75/1.28 addNat( X, suc( X ) ) }.
% 0.75/1.28 parent0[0]: (2636) {G1,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) ==>
% 0.75/1.28 proj1Suc( double( suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (128) {G2,W9,D5,L1,V1,M1} P(79,3) { proj1Suc( double( suc( X )
% 0.75/1.28 ) ) = addNat( X, suc( X ) ) }.
% 0.75/1.28 parent0: (2637) {G1,W9,D5,L1,V1,M1} { proj1Suc( double( suc( X ) ) ) ==>
% 0.75/1.28 addNat( X, suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2639) {G1,W9,D4,L2,V1,M2} { evenNat( double( suc( X ) ) ),
% 0.75/1.28 evenNat( addNat( X, suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (79) {G1,W9,D5,L1,V1,M1} P(18,19) { suc( addNat( X, suc( X ) )
% 0.75/1.28 ) ==> double( suc( X ) ) }.
% 0.75/1.28 parent1[1; 1]: (11) {G0,W5,D3,L2,V1,M2} I { evenNat( X ), evenNat( suc( X )
% 0.75/1.28 ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := addNat( X, suc( X ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (130) {G2,W9,D4,L2,V1,M2} P(79,11) { evenNat( addNat( X, suc(
% 0.75/1.28 X ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 parent0: (2639) {G1,W9,D4,L2,V1,M2} { evenNat( double( suc( X ) ) ),
% 0.75/1.28 evenNat( addNat( X, suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 1
% 0.75/1.28 1 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2641) {G1,W9,D5,L1,V1,M1} { double( suc( X ) ) ==> suc( addNat( X
% 0.75/1.28 , suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (79) {G1,W9,D5,L1,V1,M1} P(18,19) { suc( addNat( X, suc( X ) )
% 0.75/1.28 ) ==> double( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2642) {G1,W7,D4,L1,V0,M1} { double( suc( zero ) ) ==> suc( suc(
% 0.75/1.28 zero ) ) }.
% 0.75/1.28 parent0[0]: (17) {G0,W5,D3,L1,V1,M1} I { addNat( zero, X ) ==> X }.
% 0.75/1.28 parent1[0; 5]: (2641) {G1,W9,D5,L1,V1,M1} { double( suc( X ) ) ==> suc(
% 0.75/1.28 addNat( X, suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := suc( zero )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := zero
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (131) {G2,W7,D4,L1,V0,M1} P(17,79) { double( suc( zero ) ) ==>
% 0.75/1.28 suc( suc( zero ) ) }.
% 0.75/1.28 parent0: (2642) {G1,W7,D4,L1,V0,M1} { double( suc( zero ) ) ==> suc( suc(
% 0.75/1.28 zero ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2645) {G0,W11,D4,L1,V3,M1} { cons( X, append( Y, Z ) ) ==> append
% 0.75/1.28 ( cons( X, Y ), Z ) }.
% 0.75/1.28 parent0[0]: (16) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==>
% 0.75/1.28 cons( Y, append( Z, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := Z
% 0.75/1.28 Y := X
% 0.75/1.28 Z := Y
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2647) {G1,W14,D6,L1,V1,M1} { cons( o, append( shw( suc( zero ) )
% 0.75/1.28 , X ) ) ==> append( shw( suc( suc( zero ) ) ), X ) }.
% 0.75/1.28 parent0[0]: (41) {G3,W10,D5,L1,V0,M1} R(13,28);d(8);d(6) { cons( o, shw(
% 0.75/1.28 suc( zero ) ) ) ==> shw( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent1[0; 9]: (2645) {G0,W11,D4,L1,V3,M1} { cons( X, append( Y, Z ) ) ==>
% 0.75/1.28 append( cons( X, Y ), Z ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := o
% 0.75/1.28 Y := shw( suc( zero ) )
% 0.75/1.28 Z := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2648) {G2,W12,D6,L1,V1,M1} { cons( o, cons( i, X ) ) ==> append
% 0.75/1.28 ( shw( suc( suc( zero ) ) ), X ) }.
% 0.75/1.28 parent0[0]: (70) {G3,W9,D5,L1,V1,M1} P(62,16);d(15) { append( shw( suc(
% 0.75/1.28 zero ) ), X ) ==> cons( i, X ) }.
% 0.75/1.28 parent1[0; 3]: (2647) {G1,W14,D6,L1,V1,M1} { cons( o, append( shw( suc(
% 0.75/1.28 zero ) ), X ) ) ==> append( shw( suc( suc( zero ) ) ), X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2649) {G2,W12,D6,L1,V1,M1} { append( shw( suc( suc( zero ) ) ), X
% 0.75/1.28 ) ==> cons( o, cons( i, X ) ) }.
% 0.75/1.28 parent0[0]: (2648) {G2,W12,D6,L1,V1,M1} { cons( o, cons( i, X ) ) ==>
% 0.75/1.28 append( shw( suc( suc( zero ) ) ), X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (150) {G4,W12,D6,L1,V1,M1} P(41,16);d(70) { append( shw( suc(
% 0.75/1.28 suc( zero ) ) ), X ) ==> cons( o, cons( i, X ) ) }.
% 0.75/1.28 parent0: (2649) {G2,W12,D6,L1,V1,M1} { append( shw( suc( suc( zero ) ) ),
% 0.75/1.28 X ) ==> cons( o, cons( i, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2651) {G0,W8,D4,L1,V1,M1} { double( rd( X ) ) ==> rd( cons( o, X
% 0.75/1.28 ) ) }.
% 0.75/1.28 parent0[0]: (22) {G0,W8,D4,L1,V1,M1} I { rd( cons( o, X ) ) ==> double( rd
% 0.75/1.28 ( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2654) {G1,W11,D6,L1,V0,M1} { double( rd( shw( suc( zero ) ) ) )
% 0.75/1.28 ==> rd( shw( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 parent0[0]: (41) {G3,W10,D5,L1,V0,M1} R(13,28);d(8);d(6) { cons( o, shw(
% 0.75/1.28 suc( zero ) ) ) ==> shw( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent1[0; 7]: (2651) {G0,W8,D4,L1,V1,M1} { double( rd( X ) ) ==> rd( cons
% 0.75/1.28 ( o, X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := shw( suc( zero ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2655) {G2,W9,D6,L1,V0,M1} { double( suc( zero ) ) ==> rd( shw(
% 0.75/1.28 suc( suc( zero ) ) ) ) }.
% 0.75/1.28 parent0[0]: (95) {G3,W7,D5,L1,V0,M1} P(20,21);d(31);d(62) { rd( shw( suc(
% 0.75/1.28 zero ) ) ) ==> suc( zero ) }.
% 0.75/1.28 parent1[0; 2]: (2654) {G1,W11,D6,L1,V0,M1} { double( rd( shw( suc( zero )
% 0.75/1.28 ) ) ) ==> rd( shw( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2656) {G3,W9,D6,L1,V0,M1} { suc( suc( zero ) ) ==> rd( shw( suc
% 0.75/1.28 ( suc( zero ) ) ) ) }.
% 0.75/1.28 parent0[0]: (131) {G2,W7,D4,L1,V0,M1} P(17,79) { double( suc( zero ) ) ==>
% 0.75/1.28 suc( suc( zero ) ) }.
% 0.75/1.28 parent1[0; 1]: (2655) {G2,W9,D6,L1,V0,M1} { double( suc( zero ) ) ==> rd(
% 0.75/1.28 shw( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2657) {G3,W9,D6,L1,V0,M1} { rd( shw( suc( suc( zero ) ) ) ) ==>
% 0.75/1.28 suc( suc( zero ) ) }.
% 0.75/1.28 parent0[0]: (2656) {G3,W9,D6,L1,V0,M1} { suc( suc( zero ) ) ==> rd( shw(
% 0.75/1.28 suc( suc( zero ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (151) {G4,W9,D6,L1,V0,M1} P(41,22);d(95);d(131) { rd( shw( suc
% 0.75/1.28 ( suc( zero ) ) ) ) ==> suc( suc( zero ) ) }.
% 0.75/1.28 parent0: (2657) {G3,W9,D6,L1,V0,M1} { rd( shw( suc( suc( zero ) ) ) ) ==>
% 0.75/1.28 suc( suc( zero ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2658) {G2,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) = proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (128) {G2,W9,D5,L1,V1,M1} P(79,3) { proj1Suc( double( suc( X )
% 0.75/1.28 ) ) = addNat( X, suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2659) {G3,W9,D5,L2,V1,M2} { evenNat( proj1Suc( double( suc( X )
% 0.75/1.28 ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (2658) {G2,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) = proj1Suc
% 0.75/1.28 ( double( suc( X ) ) ) }.
% 0.75/1.28 parent1[0; 1]: (130) {G2,W9,D4,L2,V1,M2} P(79,11) { evenNat( addNat( X, suc
% 0.75/1.28 ( X ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (167) {G3,W9,D5,L2,V1,M2} P(128,130) { evenNat( proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 parent0: (2659) {G3,W9,D5,L2,V1,M2} { evenNat( proj1Suc( double( suc( X )
% 0.75/1.28 ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 1 ==> 1
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2660) {G2,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) = proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (128) {G2,W9,D5,L1,V1,M1} P(79,3) { proj1Suc( double( suc( X )
% 0.75/1.28 ) ) = addNat( X, suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2661) {G1,W9,D5,L1,V1,M1} { double( suc( X ) ) ==> suc( addNat( X
% 0.75/1.28 , suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (79) {G1,W9,D5,L1,V1,M1} P(18,19) { suc( addNat( X, suc( X ) )
% 0.75/1.28 ) ==> double( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2662) {G2,W9,D6,L1,V1,M1} { double( suc( X ) ) ==> suc( proj1Suc
% 0.75/1.28 ( double( suc( X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (2660) {G2,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) = proj1Suc
% 0.75/1.28 ( double( suc( X ) ) ) }.
% 0.75/1.28 parent1[0; 5]: (2661) {G1,W9,D5,L1,V1,M1} { double( suc( X ) ) ==> suc(
% 0.75/1.28 addNat( X, suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2663) {G2,W9,D6,L1,V1,M1} { suc( proj1Suc( double( suc( X ) ) ) )
% 0.75/1.28 ==> double( suc( X ) ) }.
% 0.75/1.28 parent0[0]: (2662) {G2,W9,D6,L1,V1,M1} { double( suc( X ) ) ==> suc(
% 0.75/1.28 proj1Suc( double( suc( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (169) {G3,W9,D6,L1,V1,M1} P(128,79) { suc( proj1Suc( double(
% 0.75/1.28 suc( X ) ) ) ) ==> double( suc( X ) ) }.
% 0.75/1.28 parent0: (2663) {G2,W9,D6,L1,V1,M1} { suc( proj1Suc( double( suc( X ) ) )
% 0.75/1.28 ) ==> double( suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2665) {G2,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) = proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (128) {G2,W9,D5,L1,V1,M1} P(79,3) { proj1Suc( double( suc( X )
% 0.75/1.28 ) ) = addNat( X, suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2669) {G2,W16,D6,L1,V1,M1} { addNat( addNat( X, suc( X ) ), suc
% 0.75/1.28 ( addNat( X, suc( X ) ) ) ) = proj1Suc( double( double( suc( X ) ) ) )
% 0.75/1.28 }.
% 0.75/1.28 parent0[0]: (79) {G1,W9,D5,L1,V1,M1} P(18,19) { suc( addNat( X, suc( X ) )
% 0.75/1.28 ) ==> double( suc( X ) ) }.
% 0.75/1.28 parent1[0; 13]: (2665) {G2,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) =
% 0.75/1.28 proj1Suc( double( suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := addNat( X, suc( X ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2670) {G2,W14,D6,L1,V1,M1} { addNat( addNat( X, suc( X ) ),
% 0.75/1.28 double( suc( X ) ) ) = proj1Suc( double( double( suc( X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (79) {G1,W9,D5,L1,V1,M1} P(18,19) { suc( addNat( X, suc( X ) )
% 0.75/1.28 ) ==> double( suc( X ) ) }.
% 0.75/1.28 parent1[0; 6]: (2669) {G2,W16,D6,L1,V1,M1} { addNat( addNat( X, suc( X ) )
% 0.75/1.28 , suc( addNat( X, suc( X ) ) ) ) = proj1Suc( double( double( suc( X ) ) )
% 0.75/1.28 ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (170) {G3,W14,D6,L1,V1,M1} P(79,128) { addNat( addNat( X, suc
% 0.75/1.28 ( X ) ), double( suc( X ) ) ) ==> proj1Suc( double( double( suc( X ) ) )
% 0.75/1.28 ) }.
% 0.75/1.28 parent0: (2670) {G2,W14,D6,L1,V1,M1} { addNat( addNat( X, suc( X ) ),
% 0.75/1.28 double( suc( X ) ) ) = proj1Suc( double( double( suc( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2675) {G2,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) = proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (128) {G2,W9,D5,L1,V1,M1} P(79,3) { proj1Suc( double( suc( X )
% 0.75/1.28 ) ) = addNat( X, suc( X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2677) {G1,W15,D6,L1,V1,M1} { addNat( double( rd( X ) ), suc(
% 0.75/1.28 double( rd( X ) ) ) ) = proj1Suc( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd(
% 0.75/1.28 cons( i, X ) ) }.
% 0.75/1.28 parent1[0; 11]: (2675) {G2,W9,D5,L1,V1,M1} { addNat( X, suc( X ) ) =
% 0.75/1.28 proj1Suc( double( suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := double( rd( X ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2678) {G1,W15,D6,L1,V1,M1} { addNat( double( rd( X ) ), rd( cons
% 0.75/1.28 ( i, X ) ) ) = proj1Suc( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd(
% 0.75/1.28 cons( i, X ) ) }.
% 0.75/1.28 parent1[0; 5]: (2677) {G1,W15,D6,L1,V1,M1} { addNat( double( rd( X ) ),
% 0.75/1.28 suc( double( rd( X ) ) ) ) = proj1Suc( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (171) {G3,W15,D6,L1,V1,M1} P(21,128) { addNat( double( rd( X )
% 0.75/1.28 ), rd( cons( i, X ) ) ) ==> proj1Suc( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 parent0: (2678) {G1,W15,D6,L1,V1,M1} { addNat( double( rd( X ) ), rd( cons
% 0.75/1.28 ( i, X ) ) ) = proj1Suc( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2683) {G0,W10,D5,L1,V2,M1} { x( X, Y ) ==> rd( append( shw( X ),
% 0.75/1.28 shw( Y ) ) ) }.
% 0.75/1.28 parent0[0]: (23) {G0,W10,D5,L1,V2,M1} I { rd( append( shw( X ), shw( Y ) )
% 0.75/1.28 ) ==> x( X, Y ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 Y := Y
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2684) {G1,W10,D5,L1,V1,M1} { x( suc( zero ), X ) ==> rd( cons( i
% 0.75/1.28 , shw( X ) ) ) }.
% 0.75/1.28 parent0[0]: (70) {G3,W9,D5,L1,V1,M1} P(62,16);d(15) { append( shw( suc(
% 0.75/1.28 zero ) ), X ) ==> cons( i, X ) }.
% 0.75/1.28 parent1[0; 6]: (2683) {G0,W10,D5,L1,V2,M1} { x( X, Y ) ==> rd( append( shw
% 0.75/1.28 ( X ), shw( Y ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := shw( X )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := suc( zero )
% 0.75/1.28 Y := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2685) {G1,W10,D5,L1,V1,M1} { rd( cons( i, shw( X ) ) ) ==> x( suc
% 0.75/1.28 ( zero ), X ) }.
% 0.75/1.28 parent0[0]: (2684) {G1,W10,D5,L1,V1,M1} { x( suc( zero ), X ) ==> rd( cons
% 0.75/1.28 ( i, shw( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (173) {G4,W10,D5,L1,V1,M1} P(70,23) { rd( cons( i, shw( X ) )
% 0.75/1.28 ) ==> x( suc( zero ), X ) }.
% 0.75/1.28 parent0: (2685) {G1,W10,D5,L1,V1,M1} { rd( cons( i, shw( X ) ) ) ==> x(
% 0.75/1.28 suc( zero ), X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 resolution: (2687) {G1,W10,D5,L2,V1,M2} { ! evenNat( suc( double( suc( X )
% 0.75/1.28 ) ) ), evenNat( proj1Suc( double( suc( X ) ) ) ) }.
% 0.75/1.28 parent0[1]: (10) {G0,W5,D3,L2,V1,M2} I { ! evenNat( suc( X ) ), ! evenNat(
% 0.75/1.28 X ) }.
% 0.75/1.28 parent1[1]: (167) {G3,W9,D5,L2,V1,M2} P(128,130) { evenNat( proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := double( suc( X ) )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (193) {G4,W10,D5,L2,V1,M2} R(167,10) { evenNat( proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) ), ! evenNat( suc( double( suc( X ) ) ) ) }.
% 0.75/1.28 parent0: (2687) {G1,W10,D5,L2,V1,M2} { ! evenNat( suc( double( suc( X ) )
% 0.75/1.28 ) ), evenNat( proj1Suc( double( suc( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 1
% 0.75/1.28 1 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2690) {G1,W13,D7,L2,V1,M2} { evenNat( double( rd( cons( i, X ) )
% 0.75/1.28 ) ), evenNat( proj1Suc( double( suc( double( rd( X ) ) ) ) ) ) }.
% 0.75/1.28 parent0[0]: (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd(
% 0.75/1.28 cons( i, X ) ) }.
% 0.75/1.28 parent1[1; 2]: (167) {G3,W9,D5,L2,V1,M2} P(128,130) { evenNat( proj1Suc(
% 0.75/1.28 double( suc( X ) ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := double( rd( X ) )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2691) {G1,W13,D6,L2,V1,M2} { evenNat( proj1Suc( double( rd( cons
% 0.75/1.28 ( i, X ) ) ) ) ), evenNat( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (21) {G0,W9,D5,L1,V1,M1} I { suc( double( rd( X ) ) ) ==> rd(
% 0.75/1.28 cons( i, X ) ) }.
% 0.75/1.28 parent1[1; 3]: (2690) {G1,W13,D7,L2,V1,M2} { evenNat( double( rd( cons( i
% 0.75/1.28 , X ) ) ) ), evenNat( proj1Suc( double( suc( double( rd( X ) ) ) ) ) )
% 0.75/1.28 }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (195) {G4,W13,D6,L2,V1,M2} P(21,167) { evenNat( proj1Suc(
% 0.75/1.28 double( rd( cons( i, X ) ) ) ) ), evenNat( double( rd( cons( i, X ) ) ) )
% 0.75/1.28 }.
% 0.75/1.28 parent0: (2691) {G1,W13,D6,L2,V1,M2} { evenNat( proj1Suc( double( rd( cons
% 0.75/1.28 ( i, X ) ) ) ) ), evenNat( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 1 ==> 1
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2693) {G2,W10,D5,L2,V1,M2} { ! evenNat( x( suc( zero ), X ) ), !
% 0.75/1.28 evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (173) {G4,W10,D5,L1,V1,M1} P(70,23) { rd( cons( i, shw( X ) ) )
% 0.75/1.28 ==> x( suc( zero ), X ) }.
% 0.75/1.28 parent1[0; 2]: (93) {G1,W9,D4,L2,V1,M2} P(21,10) { ! evenNat( rd( cons( i,
% 0.75/1.28 X ) ) ), ! evenNat( double( rd( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := shw( X )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (320) {G5,W10,D5,L2,V1,M2} P(173,93) { ! evenNat( x( suc( zero
% 0.75/1.28 ), X ) ), ! evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 parent0: (2693) {G2,W10,D5,L2,V1,M2} { ! evenNat( x( suc( zero ), X ) ), !
% 0.75/1.28 evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 1 ==> 1
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2695) {G1,W10,D5,L2,V1,M2} { ! evenNat( x( X, suc( zero ) ) ), !
% 0.75/1.28 evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (24) {G0,W7,D3,L1,V2,M1} I { x( X, Y ) = x( Y, X ) }.
% 0.75/1.28 parent1[0; 2]: (320) {G5,W10,D5,L2,V1,M2} P(173,93) { ! evenNat( x( suc(
% 0.75/1.28 zero ), X ) ), ! evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := suc( zero )
% 0.75/1.28 Y := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (395) {G6,W10,D5,L2,V1,M2} P(24,320) { ! evenNat( x( X, suc(
% 0.75/1.28 zero ) ) ), ! evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 parent0: (2695) {G1,W10,D5,L2,V1,M2} { ! evenNat( x( X, suc( zero ) ) ), !
% 0.75/1.28 evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 1 ==> 1
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2698) {G4,W10,D5,L1,V1,M1} { x( suc( zero ), X ) ==> rd( cons( i
% 0.75/1.28 , shw( X ) ) ) }.
% 0.75/1.28 parent0[0]: (173) {G4,W10,D5,L1,V1,M1} P(70,23) { rd( cons( i, shw( X ) ) )
% 0.75/1.28 ==> x( suc( zero ), X ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2701) {G5,W12,D7,L1,V0,M1} { x( suc( zero ), suc( zero ) ) ==>
% 0.75/1.28 rd( shw( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.28 parent0[0]: (61) {G4,W11,D6,L1,V0,M1} R(14,29);d(8);d(7) { cons( i, shw(
% 0.75/1.28 suc( zero ) ) ) ==> shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.28 parent1[0; 7]: (2698) {G4,W10,D5,L1,V1,M1} { x( suc( zero ), X ) ==> rd(
% 0.75/1.28 cons( i, shw( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := suc( zero )
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2702) {G6,W10,D5,L1,V0,M1} { x( suc( zero ), suc( zero ) ) ==>
% 0.75/1.28 suc( double( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (99) {G5,W11,D7,L1,V0,M1} P(95,21);d(61) { rd( shw( suc( suc(
% 0.75/1.28 suc( zero ) ) ) ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 parent1[0; 6]: (2701) {G5,W12,D7,L1,V0,M1} { x( suc( zero ), suc( zero ) )
% 0.75/1.28 ==> rd( shw( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2703) {G3,W10,D5,L1,V0,M1} { x( suc( zero ), suc( zero ) ) ==>
% 0.75/1.28 suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (131) {G2,W7,D4,L1,V0,M1} P(17,79) { double( suc( zero ) ) ==>
% 0.75/1.28 suc( suc( zero ) ) }.
% 0.75/1.28 parent1[0; 7]: (2702) {G6,W10,D5,L1,V0,M1} { x( suc( zero ), suc( zero ) )
% 0.75/1.28 ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (489) {G6,W10,D5,L1,V0,M1} P(61,173);d(99);d(131) { x( suc(
% 0.75/1.28 zero ), suc( zero ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0: (2703) {G3,W10,D5,L1,V0,M1} { x( suc( zero ), suc( zero ) ) ==>
% 0.75/1.28 suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2707) {G3,W11,D7,L1,V0,M1} { rd( shw( suc( suc( suc( zero ) ) )
% 0.75/1.28 ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (131) {G2,W7,D4,L1,V0,M1} P(17,79) { double( suc( zero ) ) ==>
% 0.75/1.28 suc( suc( zero ) ) }.
% 0.75/1.28 parent1[0; 8]: (99) {G5,W11,D7,L1,V0,M1} P(95,21);d(61) { rd( shw( suc( suc
% 0.75/1.28 ( suc( zero ) ) ) ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (1072) {G6,W11,D7,L1,V0,M1} S(99);d(131) { rd( shw( suc( suc(
% 0.75/1.28 suc( zero ) ) ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0: (2707) {G3,W11,D7,L1,V0,M1} { rd( shw( suc( suc( suc( zero ) ) )
% 0.75/1.28 ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2710) {G0,W10,D5,L1,V2,M1} { x( X, Y ) ==> rd( append( shw( X ),
% 0.75/1.28 shw( Y ) ) ) }.
% 0.75/1.28 parent0[0]: (23) {G0,W10,D5,L1,V2,M1} I { rd( append( shw( X ), shw( Y ) )
% 0.75/1.28 ) ==> x( X, Y ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 Y := Y
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2713) {G1,W13,D6,L1,V1,M1} { x( suc( suc( zero ) ), X ) ==> rd(
% 0.75/1.28 cons( o, cons( i, shw( X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (150) {G4,W12,D6,L1,V1,M1} P(41,16);d(70) { append( shw( suc(
% 0.75/1.28 suc( zero ) ) ), X ) ==> cons( o, cons( i, X ) ) }.
% 0.75/1.28 parent1[0; 7]: (2710) {G0,W10,D5,L1,V2,M1} { x( X, Y ) ==> rd( append( shw
% 0.75/1.28 ( X ), shw( Y ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := shw( X )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := suc( suc( zero ) )
% 0.75/1.28 Y := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2714) {G1,W12,D6,L1,V1,M1} { x( suc( suc( zero ) ), X ) ==>
% 0.75/1.28 double( rd( cons( i, shw( X ) ) ) ) }.
% 0.75/1.28 parent0[0]: (22) {G0,W8,D4,L1,V1,M1} I { rd( cons( o, X ) ) ==> double( rd
% 0.75/1.28 ( X ) ) }.
% 0.75/1.28 parent1[0; 6]: (2713) {G1,W13,D6,L1,V1,M1} { x( suc( suc( zero ) ), X )
% 0.75/1.28 ==> rd( cons( o, cons( i, shw( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := cons( i, shw( X ) )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2715) {G2,W11,D5,L1,V1,M1} { x( suc( suc( zero ) ), X ) ==>
% 0.75/1.28 double( x( suc( zero ), X ) ) }.
% 0.75/1.28 parent0[0]: (173) {G4,W10,D5,L1,V1,M1} P(70,23) { rd( cons( i, shw( X ) ) )
% 0.75/1.28 ==> x( suc( zero ), X ) }.
% 0.75/1.28 parent1[0; 7]: (2714) {G1,W12,D6,L1,V1,M1} { x( suc( suc( zero ) ), X )
% 0.75/1.28 ==> double( rd( cons( i, shw( X ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (1478) {G5,W11,D5,L1,V1,M1} P(150,23);d(22);d(173) { x( suc(
% 0.75/1.28 suc( zero ) ), X ) ==> double( x( suc( zero ), X ) ) }.
% 0.75/1.28 parent0: (2715) {G2,W11,D5,L1,V1,M1} { x( suc( suc( zero ) ), X ) ==>
% 0.75/1.28 double( x( suc( zero ), X ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 eqswap: (2718) {G3,W14,D6,L1,V1,M1} { proj1Suc( double( double( suc( X ) )
% 0.75/1.28 ) ) ==> addNat( addNat( X, suc( X ) ), double( suc( X ) ) ) }.
% 0.75/1.28 parent0[0]: (170) {G3,W14,D6,L1,V1,M1} P(79,128) { addNat( addNat( X, suc(
% 0.75/1.28 X ) ), double( suc( X ) ) ) ==> proj1Suc( double( double( suc( X ) ) ) )
% 0.75/1.28 }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := X
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2722) {G1,W12,D6,L1,V0,M1} { proj1Suc( double( double( suc( zero
% 0.75/1.28 ) ) ) ) ==> addNat( suc( zero ), double( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (17) {G0,W5,D3,L1,V1,M1} I { addNat( zero, X ) ==> X }.
% 0.75/1.28 parent1[0; 7]: (2718) {G3,W14,D6,L1,V1,M1} { proj1Suc( double( double( suc
% 0.75/1.28 ( X ) ) ) ) ==> addNat( addNat( X, suc( X ) ), double( suc( X ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := suc( zero )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 X := zero
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2723) {G1,W12,D6,L1,V0,M1} { proj1Suc( double( double( suc( zero
% 0.75/1.28 ) ) ) ) ==> suc( addNat( zero, double( suc( zero ) ) ) ) }.
% 0.75/1.28 parent0[0]: (18) {G0,W9,D4,L1,V2,M1} I { addNat( suc( Y ), X ) ==> suc(
% 0.75/1.28 addNat( Y, X ) ) }.
% 0.75/1.28 parent1[0; 6]: (2722) {G1,W12,D6,L1,V0,M1} { proj1Suc( double( double( suc
% 0.75/1.28 ( zero ) ) ) ) ==> addNat( suc( zero ), double( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := double( suc( zero ) )
% 0.75/1.28 Y := zero
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2724) {G1,W10,D6,L1,V0,M1} { proj1Suc( double( double( suc( zero
% 0.75/1.28 ) ) ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (17) {G0,W5,D3,L1,V1,M1} I { addNat( zero, X ) ==> X }.
% 0.75/1.28 parent1[0; 7]: (2723) {G1,W12,D6,L1,V0,M1} { proj1Suc( double( double( suc
% 0.75/1.28 ( zero ) ) ) ) ==> suc( addNat( zero, double( suc( zero ) ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 X := double( suc( zero ) )
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2726) {G2,W10,D6,L1,V0,M1} { proj1Suc( double( double( suc( zero
% 0.75/1.28 ) ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (131) {G2,W7,D4,L1,V0,M1} P(17,79) { double( suc( zero ) ) ==>
% 0.75/1.28 suc( suc( zero ) ) }.
% 0.75/1.28 parent1[0; 7]: (2724) {G1,W10,D6,L1,V0,M1} { proj1Suc( double( double( suc
% 0.75/1.28 ( zero ) ) ) ) ==> suc( double( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2727) {G3,W10,D6,L1,V0,M1} { proj1Suc( double( suc( suc( zero )
% 0.75/1.28 ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 parent0[0]: (131) {G2,W7,D4,L1,V0,M1} P(17,79) { double( suc( zero ) ) ==>
% 0.75/1.28 suc( suc( zero ) ) }.
% 0.75/1.28 parent1[0; 3]: (2726) {G2,W10,D6,L1,V0,M1} { proj1Suc( double( double( suc
% 0.75/1.28 ( zero ) ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 substitution1:
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 subsumption: (1712) {G4,W10,D6,L1,V0,M1} P(17,170);d(18);d(17);d(131) {
% 0.75/1.28 proj1Suc( double( suc( suc( zero ) ) ) ) ==> suc( suc( suc( zero ) ) )
% 0.75/1.28 }.
% 0.75/1.28 parent0: (2727) {G3,W10,D6,L1,V0,M1} { proj1Suc( double( suc( suc( zero )
% 0.75/1.28 ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.28 substitution0:
% 0.75/1.28 end
% 0.75/1.28 permutation0:
% 0.75/1.28 0 ==> 0
% 0.75/1.28 end
% 0.75/1.28
% 0.75/1.28 paramod: (2732) {G5,W11,D6,L2,V0,M2} { evenNat( suc( suc( suc( zero ) ) )
% 0.75/1.28 ), ! evenNat( suc( double( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.28 parent0[0]: (1712) {G4,W10,D6,L1,V0,M1} P(17,170);d(18);d(17);d(131) {
% 0.75/1.28 proj1Suc( double( suc( suc( zero ) ) ) ) ==> suc( suc( suc( zero ) ) )
% 0.75/1.29 }.
% 0.75/1.29 parent1[0; 1]: (193) {G4,W10,D5,L2,V1,M2} R(167,10) { evenNat( proj1Suc(
% 0.75/1.29 double( suc( X ) ) ) ), ! evenNat( suc( double( suc( X ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 X := suc( zero )
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 resolution: (2733) {G4,W6,D6,L1,V0,M1} { ! evenNat( suc( double( suc( suc
% 0.75/1.29 ( zero ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (29) {G3,W5,D5,L1,V0,M1} R(28,10) { ! evenNat( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) }.
% 0.75/1.29 parent1[0]: (2732) {G5,W11,D6,L2,V0,M2} { evenNat( suc( suc( suc( zero ) )
% 0.75/1.29 ) ), ! evenNat( suc( double( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 subsumption: (1714) {G5,W6,D6,L1,V0,M1} P(1712,193);r(29) { ! evenNat( suc
% 0.75/1.29 ( double( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 parent0: (2733) {G4,W6,D6,L1,V0,M1} { ! evenNat( suc( double( suc( suc(
% 0.75/1.29 zero ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 permutation0:
% 0.75/1.29 0 ==> 0
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 eqswap: (2735) {G3,W9,D6,L1,V1,M1} { double( suc( X ) ) ==> suc( proj1Suc
% 0.75/1.29 ( double( suc( X ) ) ) ) }.
% 0.75/1.29 parent0[0]: (169) {G3,W9,D6,L1,V1,M1} P(128,79) { suc( proj1Suc( double(
% 0.75/1.29 suc( X ) ) ) ) ==> double( suc( X ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 X := X
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2736) {G4,W10,D6,L1,V0,M1} { double( suc( suc( zero ) ) ) ==>
% 0.75/1.29 suc( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent0[0]: (1712) {G4,W10,D6,L1,V0,M1} P(17,170);d(18);d(17);d(131) {
% 0.75/1.29 proj1Suc( double( suc( suc( zero ) ) ) ) ==> suc( suc( suc( zero ) ) )
% 0.75/1.29 }.
% 0.75/1.29 parent1[0; 6]: (2735) {G3,W9,D6,L1,V1,M1} { double( suc( X ) ) ==> suc(
% 0.75/1.29 proj1Suc( double( suc( X ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 X := suc( zero )
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 eqswap: (2737) {G4,W10,D6,L1,V0,M1} { suc( suc( suc( suc( zero ) ) ) ) ==>
% 0.75/1.29 double( suc( suc( zero ) ) ) }.
% 0.75/1.29 parent0[0]: (2736) {G4,W10,D6,L1,V0,M1} { double( suc( suc( zero ) ) ) ==>
% 0.75/1.29 suc( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 subsumption: (1715) {G5,W10,D6,L1,V0,M1} P(1712,169) { suc( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ==> double( suc( suc( zero ) ) ) }.
% 0.75/1.29 parent0: (2737) {G4,W10,D6,L1,V0,M1} { suc( suc( suc( suc( zero ) ) ) )
% 0.75/1.29 ==> double( suc( suc( zero ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 permutation0:
% 0.75/1.29 0 ==> 0
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2739) {G4,W10,D5,L2,V0,M2} { evenNat( suc( suc( suc( zero ) ) )
% 0.75/1.29 ), evenNat( double( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent0[0]: (1712) {G4,W10,D6,L1,V0,M1} P(17,170);d(18);d(17);d(131) {
% 0.75/1.29 proj1Suc( double( suc( suc( zero ) ) ) ) ==> suc( suc( suc( zero ) ) )
% 0.75/1.29 }.
% 0.75/1.29 parent1[0; 1]: (167) {G3,W9,D5,L2,V1,M2} P(128,130) { evenNat( proj1Suc(
% 0.75/1.29 double( suc( X ) ) ) ), evenNat( double( suc( X ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 X := suc( zero )
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 resolution: (2740) {G4,W5,D5,L1,V0,M1} { evenNat( double( suc( suc( zero )
% 0.75/1.29 ) ) ) }.
% 0.75/1.29 parent0[0]: (29) {G3,W5,D5,L1,V0,M1} R(28,10) { ! evenNat( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) }.
% 0.75/1.29 parent1[0]: (2739) {G4,W10,D5,L2,V0,M2} { evenNat( suc( suc( suc( zero ) )
% 0.75/1.29 ) ), evenNat( double( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 subsumption: (1716) {G5,W5,D5,L1,V0,M1} P(1712,167);r(29) { evenNat( double
% 0.75/1.29 ( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent0: (2740) {G4,W5,D5,L1,V0,M1} { evenNat( double( suc( suc( zero ) )
% 0.75/1.29 ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 permutation0:
% 0.75/1.29 0 ==> 0
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 eqswap: (2742) {G3,W15,D6,L1,V1,M1} { proj1Suc( double( rd( cons( i, X ) )
% 0.75/1.29 ) ) ==> addNat( double( rd( X ) ), rd( cons( i, X ) ) ) }.
% 0.75/1.29 parent0[0]: (171) {G3,W15,D6,L1,V1,M1} P(21,128) { addNat( double( rd( X )
% 0.75/1.29 ), rd( cons( i, X ) ) ) ==> proj1Suc( double( rd( cons( i, X ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 X := X
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2751) {G4,W21,D8,L1,V0,M1} { proj1Suc( double( rd( cons( i, shw
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ==> addNat( double( rd( shw( suc( zero ) ) ) ),
% 0.75/1.29 rd( shw( suc( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (61) {G4,W11,D6,L1,V0,M1} R(14,29);d(8);d(7) { cons( i, shw(
% 0.75/1.29 suc( zero ) ) ) ==> shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent1[0; 16]: (2742) {G3,W15,D6,L1,V1,M1} { proj1Suc( double( rd( cons(
% 0.75/1.29 i, X ) ) ) ) ==> addNat( double( rd( X ) ), rd( cons( i, X ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 X := shw( suc( zero ) )
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2752) {G5,W21,D9,L1,V0,M1} { proj1Suc( double( rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ) ==> addNat( double( rd( shw( suc( zero ) ) ) )
% 0.75/1.29 , rd( shw( suc( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (61) {G4,W11,D6,L1,V0,M1} R(14,29);d(8);d(7) { cons( i, shw(
% 0.75/1.29 suc( zero ) ) ) ==> shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent1[0; 4]: (2751) {G4,W21,D8,L1,V0,M1} { proj1Suc( double( rd( cons( i
% 0.75/1.29 , shw( suc( zero ) ) ) ) ) ) ==> addNat( double( rd( shw( suc( zero ) ) )
% 0.75/1.29 ), rd( shw( suc( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2762) {G4,W19,D9,L1,V0,M1} { proj1Suc( double( rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ) ==> addNat( double( suc( zero ) ), rd( shw( suc
% 0.75/1.29 ( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (95) {G3,W7,D5,L1,V0,M1} P(20,21);d(31);d(62) { rd( shw( suc(
% 0.75/1.29 zero ) ) ) ==> suc( zero ) }.
% 0.75/1.29 parent1[0; 11]: (2752) {G5,W21,D9,L1,V0,M1} { proj1Suc( double( rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) ==> addNat( double( rd( shw( suc( zero
% 0.75/1.29 ) ) ) ), rd( shw( suc( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2763) {G3,W19,D9,L1,V0,M1} { proj1Suc( double( rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ) ==> addNat( suc( suc( zero ) ), rd( shw( suc(
% 0.75/1.29 suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (131) {G2,W7,D4,L1,V0,M1} P(17,79) { double( suc( zero ) ) ==>
% 0.75/1.29 suc( suc( zero ) ) }.
% 0.75/1.29 parent1[0; 10]: (2762) {G4,W19,D9,L1,V0,M1} { proj1Suc( double( rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) ==> addNat( double( suc( zero ) ), rd(
% 0.75/1.29 shw( suc( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2764) {G1,W19,D9,L1,V0,M1} { proj1Suc( double( rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ) ==> suc( addNat( suc( zero ), rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (18) {G0,W9,D4,L1,V2,M1} I { addNat( suc( Y ), X ) ==> suc(
% 0.75/1.29 addNat( Y, X ) ) }.
% 0.75/1.29 parent1[0; 9]: (2763) {G3,W19,D9,L1,V0,M1} { proj1Suc( double( rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) ==> addNat( suc( suc( zero ) ), rd( shw
% 0.75/1.29 ( suc( suc( suc( zero ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 X := rd( shw( suc( suc( suc( zero ) ) ) ) )
% 0.75/1.29 Y := suc( zero )
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2766) {G1,W19,D10,L1,V0,M1} { proj1Suc( double( rd( shw( suc(
% 0.75/1.29 suc( suc( zero ) ) ) ) ) ) ) ==> suc( suc( addNat( zero, rd( shw( suc(
% 0.75/1.29 suc( suc( zero ) ) ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (18) {G0,W9,D4,L1,V2,M1} I { addNat( suc( Y ), X ) ==> suc(
% 0.75/1.29 addNat( Y, X ) ) }.
% 0.75/1.29 parent1[0; 10]: (2764) {G1,W19,D9,L1,V0,M1} { proj1Suc( double( rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) ==> suc( addNat( suc( zero ), rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 X := rd( shw( suc( suc( suc( zero ) ) ) ) )
% 0.75/1.29 Y := zero
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2767) {G1,W17,D9,L1,V0,M1} { proj1Suc( double( rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ) ==> suc( suc( rd( shw( suc( suc( suc( zero ) )
% 0.75/1.29 ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (17) {G0,W5,D3,L1,V1,M1} I { addNat( zero, X ) ==> X }.
% 0.75/1.29 parent1[0; 11]: (2766) {G1,W19,D10,L1,V0,M1} { proj1Suc( double( rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) ==> suc( suc( addNat( zero, rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 X := rd( shw( suc( suc( suc( zero ) ) ) ) )
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2769) {G2,W15,D9,L1,V0,M1} { proj1Suc( double( rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ) ==> suc( suc( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (1072) {G6,W11,D7,L1,V0,M1} S(99);d(131) { rd( shw( suc( suc(
% 0.75/1.29 suc( zero ) ) ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.29 parent1[0; 11]: (2767) {G1,W17,D9,L1,V0,M1} { proj1Suc( double( rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) ==> suc( suc( rd( shw( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2770) {G3,W13,D7,L1,V0,M1} { proj1Suc( double( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ) ==> suc( suc( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (1072) {G6,W11,D7,L1,V0,M1} S(99);d(131) { rd( shw( suc( suc(
% 0.75/1.29 suc( zero ) ) ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.29 parent1[0; 3]: (2769) {G2,W15,D9,L1,V0,M1} { proj1Suc( double( rd( shw(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ) ) ==> suc( suc( suc( suc( suc( zero ) ) )
% 0.75/1.29 ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2773) {G4,W12,D7,L1,V0,M1} { proj1Suc( double( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ) ==> suc( double( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent0[0]: (1715) {G5,W10,D6,L1,V0,M1} P(1712,169) { suc( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ==> double( suc( suc( zero ) ) ) }.
% 0.75/1.29 parent1[0; 8]: (2770) {G3,W13,D7,L1,V0,M1} { proj1Suc( double( suc( suc(
% 0.75/1.29 suc( zero ) ) ) ) ) ==> suc( suc( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 subsumption: (1767) {G7,W12,D7,L1,V0,M1} P(61,171);d(95);d(131);d(18);d(18)
% 0.75/1.29 ;d(17);d(1072);d(1715) { proj1Suc( double( suc( suc( suc( zero ) ) ) ) )
% 0.75/1.29 ==> suc( double( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent0: (2773) {G4,W12,D7,L1,V0,M1} { proj1Suc( double( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ) ==> suc( double( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 permutation0:
% 0.75/1.29 0 ==> 0
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2780) {G5,W17,D8,L2,V0,M2} { evenNat( double( rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ), evenNat( proj1Suc( double( rd( cons( i, shw(
% 0.75/1.29 suc( zero ) ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (61) {G4,W11,D6,L1,V0,M1} R(14,29);d(8);d(7) { cons( i, shw(
% 0.75/1.29 suc( zero ) ) ) ==> shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent1[1; 3]: (195) {G4,W13,D6,L2,V1,M2} P(21,167) { evenNat( proj1Suc(
% 0.75/1.29 double( rd( cons( i, X ) ) ) ) ), evenNat( double( rd( cons( i, X ) ) ) )
% 0.75/1.29 }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 X := shw( suc( zero ) )
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2781) {G5,W17,D9,L2,V0,M2} { evenNat( proj1Suc( double( rd( shw
% 0.75/1.29 ( suc( suc( suc( zero ) ) ) ) ) ) ) ), evenNat( double( rd( shw( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (61) {G4,W11,D6,L1,V0,M1} R(14,29);d(8);d(7) { cons( i, shw(
% 0.75/1.29 suc( zero ) ) ) ==> shw( suc( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent1[1; 4]: (2780) {G5,W17,D8,L2,V0,M2} { evenNat( double( rd( shw( suc
% 0.75/1.29 ( suc( suc( zero ) ) ) ) ) ) ), evenNat( proj1Suc( double( rd( cons( i,
% 0.75/1.29 shw( suc( zero ) ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2784) {G6,W15,D9,L2,V0,M2} { evenNat( double( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ), evenNat( proj1Suc( double( rd( shw( suc( suc( suc( zero )
% 0.75/1.29 ) ) ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (1072) {G6,W11,D7,L1,V0,M1} S(99);d(131) { rd( shw( suc( suc(
% 0.75/1.29 suc( zero ) ) ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.29 parent1[1; 2]: (2781) {G5,W17,D9,L2,V0,M2} { evenNat( proj1Suc( double( rd
% 0.75/1.29 ( shw( suc( suc( suc( zero ) ) ) ) ) ) ) ), evenNat( double( rd( shw( suc
% 0.75/1.29 ( suc( suc( zero ) ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2786) {G7,W13,D7,L2,V0,M2} { evenNat( proj1Suc( double( suc( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ) ), evenNat( double( suc( suc( suc( zero ) ) ) ) )
% 0.75/1.29 }.
% 0.75/1.29 parent0[0]: (1072) {G6,W11,D7,L1,V0,M1} S(99);d(131) { rd( shw( suc( suc(
% 0.75/1.29 suc( zero ) ) ) ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.29 parent1[1; 3]: (2784) {G6,W15,D9,L2,V0,M2} { evenNat( double( suc( suc(
% 0.75/1.29 suc( zero ) ) ) ) ), evenNat( proj1Suc( double( rd( shw( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2787) {G8,W12,D6,L2,V0,M2} { evenNat( suc( double( suc( suc(
% 0.75/1.29 zero ) ) ) ) ), evenNat( double( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (1767) {G7,W12,D7,L1,V0,M1} P(61,171);d(95);d(131);d(18);d(18);
% 0.75/1.29 d(17);d(1072);d(1715) { proj1Suc( double( suc( suc( suc( zero ) ) ) ) )
% 0.75/1.29 ==> suc( double( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent1[0; 1]: (2786) {G7,W13,D7,L2,V0,M2} { evenNat( proj1Suc( double(
% 0.75/1.29 suc( suc( suc( zero ) ) ) ) ) ), evenNat( double( suc( suc( suc( zero ) )
% 0.75/1.29 ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 resolution: (2788) {G6,W6,D6,L1,V0,M1} { evenNat( double( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (1714) {G5,W6,D6,L1,V0,M1} P(1712,193);r(29) { ! evenNat( suc(
% 0.75/1.29 double( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 parent1[0]: (2787) {G8,W12,D6,L2,V0,M2} { evenNat( suc( double( suc( suc(
% 0.75/1.29 zero ) ) ) ) ), evenNat( double( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 subsumption: (2142) {G8,W6,D6,L1,V0,M1} P(61,195);d(1072);d(1072);d(1767);r
% 0.75/1.29 (1714) { evenNat( double( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 parent0: (2788) {G6,W6,D6,L1,V0,M1} { evenNat( double( suc( suc( suc( zero
% 0.75/1.29 ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 permutation0:
% 0.75/1.29 0 ==> 0
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2792) {G6,W14,D7,L2,V0,M2} { ! evenNat( double( x( suc( zero ),
% 0.75/1.29 suc( zero ) ) ) ), ! evenNat( double( rd( shw( suc( suc( zero ) ) ) ) ) )
% 0.75/1.29 }.
% 0.75/1.29 parent0[0]: (1478) {G5,W11,D5,L1,V1,M1} P(150,23);d(22);d(173) { x( suc(
% 0.75/1.29 suc( zero ) ), X ) ==> double( x( suc( zero ), X ) ) }.
% 0.75/1.29 parent1[0; 2]: (395) {G6,W10,D5,L2,V1,M2} P(24,320) { ! evenNat( x( X, suc
% 0.75/1.29 ( zero ) ) ), ! evenNat( double( rd( shw( X ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 X := suc( zero )
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 X := suc( suc( zero ) )
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2793) {G7,W13,D7,L2,V0,M2} { ! evenNat( double( suc( suc( suc(
% 0.75/1.29 zero ) ) ) ) ), ! evenNat( double( rd( shw( suc( suc( zero ) ) ) ) ) )
% 0.75/1.29 }.
% 0.75/1.29 parent0[0]: (489) {G6,W10,D5,L1,V0,M1} P(61,173);d(99);d(131) { x( suc(
% 0.75/1.29 zero ), suc( zero ) ) ==> suc( suc( suc( zero ) ) ) }.
% 0.75/1.29 parent1[0; 3]: (2792) {G6,W14,D7,L2,V0,M2} { ! evenNat( double( x( suc(
% 0.75/1.29 zero ), suc( zero ) ) ) ), ! evenNat( double( rd( shw( suc( suc( zero ) )
% 0.75/1.29 ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 paramod: (2794) {G5,W11,D6,L2,V0,M2} { ! evenNat( double( suc( suc( zero )
% 0.75/1.29 ) ) ), ! evenNat( double( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 parent0[0]: (151) {G4,W9,D6,L1,V0,M1} P(41,22);d(95);d(131) { rd( shw( suc
% 0.75/1.29 ( suc( zero ) ) ) ) ==> suc( suc( zero ) ) }.
% 0.75/1.29 parent1[1; 3]: (2793) {G7,W13,D7,L2,V0,M2} { ! evenNat( double( suc( suc(
% 0.75/1.29 suc( zero ) ) ) ) ), ! evenNat( double( rd( shw( suc( suc( zero ) ) ) ) )
% 0.75/1.29 ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 resolution: (2795) {G6,W5,D5,L1,V0,M1} { ! evenNat( double( suc( suc( zero
% 0.75/1.29 ) ) ) ) }.
% 0.75/1.29 parent0[1]: (2794) {G5,W11,D6,L2,V0,M2} { ! evenNat( double( suc( suc(
% 0.75/1.29 zero ) ) ) ), ! evenNat( double( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 parent1[0]: (2142) {G8,W6,D6,L1,V0,M1} P(61,195);d(1072);d(1072);d(1767);r(
% 0.75/1.29 1714) { evenNat( double( suc( suc( suc( zero ) ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 subsumption: (2284) {G9,W5,D5,L1,V0,M1} P(1478,395);d(489);d(151);r(2142)
% 0.75/1.29 { ! evenNat( double( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent0: (2795) {G6,W5,D5,L1,V0,M1} { ! evenNat( double( suc( suc( zero )
% 0.75/1.29 ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 permutation0:
% 0.75/1.29 0 ==> 0
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 resolution: (2796) {G6,W0,D0,L0,V0,M0} { }.
% 0.75/1.29 parent0[0]: (2284) {G9,W5,D5,L1,V0,M1} P(1478,395);d(489);d(151);r(2142) {
% 0.75/1.29 ! evenNat( double( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 parent1[0]: (1716) {G5,W5,D5,L1,V0,M1} P(1712,167);r(29) { evenNat( double
% 0.75/1.29 ( suc( suc( zero ) ) ) ) }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 substitution1:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 subsumption: (2287) {G10,W0,D0,L0,V0,M0} S(2284);r(1716) { }.
% 0.75/1.29 parent0: (2796) {G6,W0,D0,L0,V0,M0} { }.
% 0.75/1.29 substitution0:
% 0.75/1.29 end
% 0.75/1.29 permutation0:
% 0.75/1.29 end
% 0.75/1.29
% 0.75/1.29 Proof check complete!
% 0.75/1.29
% 0.75/1.29 Memory use:
% 0.75/1.29
% 0.75/1.29 space for terms: 31714
% 0.75/1.29 space for clauses: 156066
% 0.75/1.29
% 0.75/1.29
% 0.75/1.29 clauses generated: 16987
% 0.75/1.29 clauses kept: 2288
% 0.75/1.29 clauses selected: 489
% 0.75/1.29 clauses deleted: 64
% 0.75/1.29 clauses inuse deleted: 29
% 0.75/1.29
% 0.75/1.29 subsentry: 13602
% 0.75/1.29 literals s-matched: 10835
% 0.75/1.29 literals matched: 10835
% 0.75/1.29 full subsumption: 1066
% 0.75/1.29
% 0.75/1.29 checksum: 1915827897
% 0.75/1.29
% 0.75/1.29
% 0.75/1.29 Bliksem ended
%------------------------------------------------------------------------------