and S is the following TRS.
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
|
originates from |
#equal(z0,z1) |
→ |
#eq(z0,z1) |
(58) |
|
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
|
originates from |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
|
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
|
originates from |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
|
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
|
originates from |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
|
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
|
originates from |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
|
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
|
originates from |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
|
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
|
originates from |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
|
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
|
originates from |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
|
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
|
originates from |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
|
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
|
originates from |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
|
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
|
originates from |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
|
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
|
originates from |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
|
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
|
originates from |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
|
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
|
originates from |
bfs2(z0,z1) |
→ |
bfs2#1(dobfs(z0,z1),z1) |
(84) |
|
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
|
originates from |
bfs2#1(z0,z1) |
→ |
dobfs(z0,z1) |
(86) |
|
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
|
originates from |
dfs(z0,z1) |
→ |
dfs#1(z0,z1) |
(88) |
|
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
|
originates from |
dfs#1(::(z0,z1),z2) |
→ |
dfs#2(z0,z0,z1,z2) |
(90) |
|
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
|
originates from |
dfs#1(nil,z0) |
→ |
leaf |
(92) |
|
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
|
originates from |
dfs#2(leaf,z0,z1,z2) |
→ |
dfs(z1,z2) |
(94) |
|
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
|
originates from |
dfs#2(node(z0,z1,z2),z3,z4,z5) |
→ |
dfs#3(#equal(z0,z5),z3,z1,z2,z4,z5) |
(96) |
|
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
|
originates from |
dfs#3(#false,z0,z1,z2,z3,z4) |
→ |
dfs(::(z1,::(z2,z3)),z4) |
(98) |
|
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
|
originates from |
dfs#3(#true,z0,z1,z2,z3,z4) |
→ |
z0 |
(100) |
|
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
|
originates from |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
|
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
|
originates from |
dodfs(z0,z1) |
→ |
dfs(::(z0,nil),z1) |
(104) |
|
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
|
originates from |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
|
#and#(#false,#false) |
→ |
c |
(108) |
|
originates from |
#and(#false,#false) |
→ |
#false |
(26) |
|
#and#(#false,#true) |
→ |
c1 |
(109) |
|
originates from |
#and(#false,#true) |
→ |
#false |
(27) |
|
#and#(#true,#false) |
→ |
c2 |
(110) |
|
originates from |
#and(#true,#false) |
→ |
#false |
(28) |
|
#and#(#true,#true) |
→ |
c3 |
(111) |
|
originates from |
#and(#true,#true) |
→ |
#true |
(29) |
|
|
originates from |
|
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
|
originates from |
#eq(#0,#neg(z0)) |
→ |
#false |
(113) |
|
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
|
originates from |
#eq(#0,#pos(z0)) |
→ |
#false |
(115) |
|
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
|
originates from |
#eq(#0,#s(z0)) |
→ |
#false |
(117) |
|
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
|
originates from |
#eq(#neg(z0),#0) |
→ |
#false |
(119) |
|
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
|
originates from |
#eq(#neg(z0),#neg(z1)) |
→ |
#eq(z0,z1) |
(121) |
|
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
|
originates from |
#eq(#neg(z0),#pos(z1)) |
→ |
#false |
(123) |
|
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
|
originates from |
#eq(#pos(z0),#0) |
→ |
#false |
(125) |
|
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
|
originates from |
#eq(#pos(z0),#neg(z1)) |
→ |
#false |
(127) |
|
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
|
originates from |
#eq(#pos(z0),#pos(z1)) |
→ |
#eq(z0,z1) |
(129) |
|
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
|
originates from |
#eq(#s(z0),#0) |
→ |
#false |
(131) |
|
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
|
originates from |
#eq(#s(z0),#s(z1)) |
→ |
#eq(z0,z1) |
(133) |
|
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
|
originates from |
#eq(::(z0,z1),::(z2,z3)) |
→ |
#and(#eq(z0,z2),#eq(z1,z3)) |
(135) |
|
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
|
originates from |
#eq(::(z0,z1),leaf) |
→ |
#false |
(137) |
|
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
|
originates from |
#eq(::(z0,z1),nil) |
→ |
#false |
(139) |
|
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
|
originates from |
#eq(::(z0,z1),node(z2,z3,z4)) |
→ |
#false |
(141) |
|
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
|
originates from |
#eq(leaf,::(z0,z1)) |
→ |
#false |
(143) |
|
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
|
originates from |
#eq(leaf,leaf) |
→ |
#true |
(47) |
|
#eq#(leaf,nil) |
→ |
c22 |
(146) |
|
originates from |
#eq(leaf,nil) |
→ |
#false |
(48) |
|
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
|
originates from |
#eq(leaf,node(z0,z1,z2)) |
→ |
#false |
(147) |
|
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
|
originates from |
#eq(nil,::(z0,z1)) |
→ |
#false |
(149) |
|
#eq#(nil,leaf) |
→ |
c25 |
(151) |
|
originates from |
#eq(nil,leaf) |
→ |
#false |
(51) |
|
#eq#(nil,nil) |
→ |
c26 |
(152) |
|
originates from |
#eq(nil,nil) |
→ |
#true |
(52) |
|
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
|
originates from |
#eq(nil,node(z0,z1,z2)) |
→ |
#false |
(153) |
|
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
|
originates from |
#eq(node(z0,z1,z2),::(z3,z4)) |
→ |
#false |
(155) |
|
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
|
originates from |
#eq(node(z0,z1,z2),leaf) |
→ |
#false |
(157) |
|
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
|
originates from |
#eq(node(z0,z1,z2),nil) |
→ |
#false |
(159) |
|
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
|
originates from |
#eq(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
#and(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))) |
(161) |
|
Moreover, we add the following terms to the innermost strategy.
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
There are 104 ruless (increase limit for explicit display).
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
[appendreverse#(x1, x2)] |
= |
+ · x1 + · x2
|
[reverse#(x1)] |
= |
+ · x1
|
[#and#(x1, x2)] |
= |
+ · x1 + · x2
|
[dfs#2#(x1,...,x4)] |
= |
+ · x1 + · x2 + · x3 + · x4
|
[c21] |
= |
|
[c5] |
= |
|
[c16(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c17] |
= |
|
[c6] |
= |
|
[c51(x1, x2)] |
= |
+ · x1 + · x2
|
[c20] |
= |
|
[c34(x1)] |
= |
+ · x1
|
[c45(x1, x2)] |
= |
+ · x1 + · x2
|
[c52(x1)] |
= |
+ · x1
|
[c47(x1)] |
= |
+ · x1
|
[c32(x1)] |
= |
+ · x1
|
[c33(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[c46(x1)] |
= |
+ · x1
|
[c7] |
= |
|
[#equal#(x1, x2)] |
= |
+ · x1 + · x2
|
[c40] |
= |
|
[c23] |
= |
|
[c] |
= |
|
[c44] |
= |
|
[c8] |
= |
|
[c14] |
= |
|
[dfs#3#(x1,...,x6)] |
= |
+ · x1 + · x2 + · x3 + · x4 + · x5 + · x6
|
[c56(x1)] |
= |
+ · x1
|
[bfs#3#(x1,...,x4)] |
= |
+ · x1 + · x2 + · x3 + · x4
|
[#eq#(x1, x2)] |
= |
+ · x1 + · x2
|
[appendreverse#1#(x1, x2)] |
= |
+ · x1 + · x2
|
[c37(x1)] |
= |
+ · x1
|
[c35] |
= |
|
[dodfs#(x1, x2)] |
= |
+ · x1 + · x2
|
[c28] |
= |
|
[dfs#1#(x1, x2)] |
= |
+ · x1 + · x2
|
[c49] |
= |
|
[c3] |
= |
|
[bfs#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c25] |
= |
|
[c38(x1)] |
= |
+ · x1
|
[c1] |
= |
|
[c12] |
= |
|
[c42(x1, x2)] |
= |
+ · x1 + · x2
|
[c30] |
= |
|
[dobfs#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9(x1)] |
= |
+ · x1
|
[c13(x1)] |
= |
+ · x1
|
[c55(x1)] |
= |
+ · x1
|
[dfs#(x1, x2)] |
= |
+ · x1 + · x2
|
[c24] |
= |
|
[bfs#1#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c26] |
= |
|
[c39(x1, x2)] |
= |
+ · x1 + · x2
|
[c11] |
= |
|
[c54(x1)] |
= |
+ · x1
|
[c19] |
= |
|
[c53] |
= |
|
[bfs#2#(x1, x2)] |
= |
+ · x1 + · x2
|
[bfs2#(x1, x2)] |
= |
+ · x1 + · x2
|
[bfs2#1#(x1, x2)] |
= |
+ · x1 + · x2
|
[c31(x1,...,x5)] |
= |
+ · x1 + · x2 + · x3 + · x4 + · x5
|
[c10] |
= |
|
[c27] |
= |
|
[c41(x1)] |
= |
+ · x1
|
[c48(x1)] |
= |
+ · x1
|
[c43(x1)] |
= |
+ · x1
|
[c50(x1)] |
= |
+ · x1
|
[c4] |
= |
|
[bfs#4#(x1,...,x7)] |
= |
+ · x1 + · x2 + · x3 + · x4 + · x5 + · x6 + · x7
|
[c29] |
= |
|
[c36(x1)] |
= |
+ · x1
|
[c22] |
= |
|
[c15(x1)] |
= |
+ · x1
|
[#0] |
= |
|
[#eq(x1, x2)] |
= |
+ · x1 + · x2
|
[bfs(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[leaf] |
= |
|
[#equal(x1, x2)] |
= |
+ · x1 + · x2
|
[bfs#4(x1,...,x7)] |
= |
+ · x1 + · x2 + · x3 + · x4 + · x5 + · x6 + · x7
|
[appendreverse(x1, x2)] |
= |
+ · x1 + · x2
|
[#neg(x1)] |
= |
+ · x1
|
[dobfs(x1, x2)] |
= |
+ · x1 + · x2
|
[bfs#1(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[#and(x1, x2)] |
= |
+ · x1 + · x2
|
[nil] |
= |
|
[#false] |
= |
|
[reverse(x1)] |
= |
+ · x1
|
[appendreverse#1(x1, x2)] |
= |
+ · x1 + · x2
|
[::(x1, x2)] |
= |
+ · x1 + · x2
|
[bfs#2(x1, x2)] |
= |
+ · x1 + · x2
|
[#pos(x1)] |
= |
+ · x1
|
[#s(x1)] |
= |
+ · x1
|
[#true] |
= |
|
[node(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[bfs#3(x1,...,x4)] |
= |
+ · x1 + · x2 + · x3 + · x4
|
which has the intended complexity.
Here, only the following usable rules have been considered:
#and#(#false,#false) |
→ |
c |
(108) |
#and#(#false,#true) |
→ |
c1 |
(109) |
#and#(#true,#false) |
→ |
c2 |
(110) |
#and#(#true,#true) |
→ |
c3 |
(111) |
#eq#(#0,#0) |
→ |
c4 |
(112) |
#eq#(#0,#neg(z0)) |
→ |
c5 |
(114) |
#eq#(#0,#pos(z0)) |
→ |
c6 |
(116) |
#eq#(#0,#s(z0)) |
→ |
c7 |
(118) |
#eq#(#neg(z0),#0) |
→ |
c8 |
(120) |
#eq#(#neg(z0),#neg(z1)) |
→ |
c9(#eq#(z0,z1)) |
(122) |
#eq#(#neg(z0),#pos(z1)) |
→ |
c10 |
(124) |
#eq#(#pos(z0),#0) |
→ |
c11 |
(126) |
#eq#(#pos(z0),#neg(z1)) |
→ |
c12 |
(128) |
#eq#(#pos(z0),#pos(z1)) |
→ |
c13(#eq#(z0,z1)) |
(130) |
#eq#(#s(z0),#0) |
→ |
c14 |
(132) |
#eq#(#s(z0),#s(z1)) |
→ |
c15(#eq#(z0,z1)) |
(134) |
#eq#(::(z0,z1),::(z2,z3)) |
→ |
c16(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) |
(136) |
#eq#(::(z0,z1),leaf) |
→ |
c17 |
(138) |
#eq#(::(z0,z1),nil) |
→ |
c18 |
(140) |
#eq#(::(z0,z1),node(z2,z3,z4)) |
→ |
c19 |
(142) |
#eq#(leaf,::(z0,z1)) |
→ |
c20 |
(144) |
#eq#(leaf,leaf) |
→ |
c21 |
(145) |
#eq#(leaf,nil) |
→ |
c22 |
(146) |
#eq#(leaf,node(z0,z1,z2)) |
→ |
c23 |
(148) |
#eq#(nil,::(z0,z1)) |
→ |
c24 |
(150) |
#eq#(nil,leaf) |
→ |
c25 |
(151) |
#eq#(nil,nil) |
→ |
c26 |
(152) |
#eq#(nil,node(z0,z1,z2)) |
→ |
c27 |
(154) |
#eq#(node(z0,z1,z2),::(z3,z4)) |
→ |
c28 |
(156) |
#eq#(node(z0,z1,z2),leaf) |
→ |
c29 |
(158) |
#eq#(node(z0,z1,z2),nil) |
→ |
c30 |
(160) |
#eq#(node(z0,z1,z2),node(z3,z4,z5)) |
→ |
c31(#and#(#eq(z0,z3),#and(#eq(z1,z4),#eq(z2,z5))),#eq#(z0,z3),#and#(#eq(z1,z4),#eq(z2,z5)),#eq#(z1,z4),#eq#(z2,z5)) |
(162) |
#equal#(z0,z1) |
→ |
c32(#eq#(z0,z1)) |
(59) |
appendreverse#(z0,z1) |
→ |
c33(appendreverse#1#(z0,z1)) |
(61) |
appendreverse#1#(::(z0,z1),z2) |
→ |
c34(appendreverse#(z1,::(z0,z2))) |
(63) |
appendreverse#1#(nil,z0) |
→ |
c35 |
(65) |
bfs#(z0,z1,z2) |
→ |
c36(bfs#1#(z0,z1,z2)) |
(67) |
bfs#1#(::(z0,z1),z2,z3) |
→ |
c37(bfs#3#(z0,z2,z1,z3)) |
(69) |
bfs#1#(nil,z0,z1) |
→ |
c38(bfs#2#(z0,z1)) |
(71) |
bfs#2#(::(z0,z1),z2) |
→ |
c39(bfs#(reverse(::(z0,z1)),nil,z2),reverse#(::(z0,z1))) |
(73) |
bfs#2#(nil,z0) |
→ |
c40 |
(75) |
bfs#3#(leaf,z0,z1,z2) |
→ |
c41(bfs#(z1,z0,z2)) |
(77) |
bfs#3#(node(z0,z1,z2),z3,z4,z5) |
→ |
c42(bfs#4#(#equal(z5,z0),z3,z1,z2,z4,z5,z0),#equal#(z5,z0)) |
(79) |
bfs#4#(#false,z0,z1,z2,z3,z4,z5) |
→ |
c43(bfs#(z3,::(z2,::(z1,z0)),z4)) |
(81) |
bfs#4#(#true,z0,z1,z2,z3,z4,z5) |
→ |
c44 |
(83) |
bfs2#(z0,z1) |
→ |
c45(bfs2#1#(dobfs(z0,z1),z1),dobfs#(z0,z1)) |
(85) |
bfs2#1#(z0,z1) |
→ |
c46(dobfs#(z0,z1)) |
(87) |
dfs#(z0,z1) |
→ |
c47(dfs#1#(z0,z1)) |
(89) |
dfs#1#(::(z0,z1),z2) |
→ |
c48(dfs#2#(z0,z0,z1,z2)) |
(91) |
dfs#1#(nil,z0) |
→ |
c49 |
(93) |
dfs#2#(leaf,z0,z1,z2) |
→ |
c50(dfs#(z1,z2)) |
(95) |
dfs#2#(node(z0,z1,z2),z3,z4,z5) |
→ |
c51(dfs#3#(#equal(z0,z5),z3,z1,z2,z4,z5),#equal#(z0,z5)) |
(97) |
dfs#3#(#false,z0,z1,z2,z3,z4) |
→ |
c52(dfs#(::(z1,::(z2,z3)),z4)) |
(99) |
dfs#3#(#true,z0,z1,z2,z3,z4) |
→ |
c53 |
(101) |
dobfs#(z0,z1) |
→ |
c54(bfs#(::(z0,nil),nil,z1)) |
(103) |
dodfs#(z0,z1) |
→ |
c55(dfs#(::(z0,nil),z1)) |
(105) |
reverse#(z0) |
→ |
c56(appendreverse#(z0,nil)) |
(107) |
reverse(z0) |
→ |
appendreverse(z0,nil) |
(106) |
bfs#4(#true,z0,z1,z2,z3,z4,z5) |
→ |
node(z5,z1,z2) |
(82) |
appendreverse#1(nil,z0) |
→ |
z0 |
(64) |
dobfs(z0,z1) |
→ |
bfs(::(z0,nil),nil,z1) |
(102) |
bfs#1(::(z0,z1),z2,z3) |
→ |
bfs#3(z0,z2,z1,z3) |
(68) |
bfs#2(::(z0,z1),z2) |
→ |
bfs(reverse(::(z0,z1)),nil,z2) |
(72) |
appendreverse#1(::(z0,z1),z2) |
→ |
appendreverse(z1,::(z0,z2)) |
(62) |
bfs#4(#false,z0,z1,z2,z3,z4,z5) |
→ |
bfs(z3,::(z2,::(z1,z0)),z4) |
(80) |
appendreverse(z0,z1) |
→ |
appendreverse#1(z0,z1) |
(60) |
bfs(z0,z1,z2) |
→ |
bfs#1(z0,z1,z2) |
(66) |
bfs#3(leaf,z0,z1,z2) |
→ |
bfs(z1,z0,z2) |
(76) |
bfs#3(node(z0,z1,z2),z3,z4,z5) |
→ |
bfs#4(#equal(z5,z0),z3,z1,z2,z4,z5,z0) |
(78) |
bfs#2(nil,z0) |
→ |
leaf |
(74) |
bfs#1(nil,z0,z1) |
→ |
bfs#2(z0,z1) |
(70) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).