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).