Problem: +(x,0()) -> x -(0()) -> 0() -(-(x)) -> x -(+(x,y)) -> +(-(x),-(y)) +(x,-(x)) -> 0() +(+(x,-(x)),y) -> y *(x,0()) -> 0() *(x,1()) -> x *(x,-(y)) -> -(*(x,y)) *(*(x,-(y)),z) -> *(-(*(x,y)),z) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(*(x,+(y,z)),w) -> +(*(*(x,y),w),*(*(x,z),w)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) *(*(x,y),z) -> *(x,*(y,z)) *(x,*(y,z)) -> *(*(x,y),z) *(x,y) -> *(y,x) Proof: Church Rosser Transformation Processor: strict: weak: critical peaks: 151 -(x) <-0|0[]- -(+(x,0())) -3|[]-> +(-(x),-(0())) +(x,-(x)) <-0|[]- +(+(x,-(x)),0()) -5|[]-> 0() *(x,y) <-0|1[]- *(x,+(y,0())) -10|[]-> +(*(x,y),*(x,0())) *(*(x,y),w) <-0|0,1[]- *(*(x,+(y,0())),w) -11|[]-> +(*(*(x,y),w),*(*(x,0()),w)) +(x,y) <-0|[]- +(+(x,y),0()) -12|[]-> +(x,+(y,0())) +(x,z) <-0|0[]- +(+(x,0()),z) -12|[]-> +(x,+(0(),z)) +(x,y) <-0|1[]- +(x,+(y,0())) -13|[]-> +(+(x,y),0()) x <-0|[]- +(x,0()) -14|[]-> +(0(),x) -(0()) <-1|0[]- -(-(0())) -2|[]-> 0() +(0(),0()) <-1|1[]- +(0(),-(0())) -4|[]-> 0() +(+(0(),0()),y) <-1|0,1[]- +(+(0(),-(0())),y) -5|[]-> y *(x,0()) <-1|1[]- *(x,-(0())) -8|[]-> -(*(x,0())) *(*(x,0()),z) <-1|0,1[]- *(*(x,-(0())),z) -9|[]-> *(-(*(x,0())),z) -(x1381) <-2|0[]- -(-(-(x1381))) -2|[]-> -(x1381) +(-(x1382),x1382) <-2|1[]- +(-(x1382),-(-(x1382))) -4|[]-> 0() +(+(-(x1383),x1383),y) <-2|0,1[]- +(+(-(x1383),-(-(x1383))),y) -5|[]-> y *(x,x1384) <-2|1[]- *(x,-(-(x1384))) -8|[]-> -(*(x,-(x1384))) *(*(x,x1385),z) <-2|0,1[]- *(*(x,-(-(x1385))),z) -9|[]-> *(-(*(x,-(x1385))),z) -(+(-(x1386),-(x1387))) <-3|0[]- -(-(+(x1386,x1387))) -2|[]-> +(x1386,x1387) +(+(x1388,x1389),+(-(x1388),-(x1389))) <-3|1[]- +(+(x1388,x1389),-(+(x1388,x1389))) -4|[]-> 0() +(+(+(x1390,x1391),+(-(x1390),-(x1391))),y) <-3|0,1[]- +(+(+(x1390,x1391),-(+(x1390,x1391))),y) -5| []-> y *(x,+(-(x1392),-(x1393))) <-3|1[]- *(x,-(+(x1392,x1393))) -8|[]-> -(*(x,+(x1392,x1393))) *(*(x,+(-(x1394),-(x1395))),z) <-3|0,1[]- *(*(x,-(+(x1394,x1395))),z) -9| []-> *(-(*(x,+(x1394,x1395))),z) -(0()) <-4|0[]- -(+(x,-(x))) -3|[]-> +(-(x),-(-(x))) 0() <-4|[]- +(+(x,-(x)),-(+(x,-(x)))) -5|[]-> -(+(x,-(x))) +(0(),y) <-4|0[]- +(+(x,-(x)),y) -5|[]-> y *(x,0()) <-4|1[]- *(x,+(y,-(y))) -10|[]-> +(*(x,y),*(x,-(y))) *(*(x,0()),w) <-4|0,1[]- *(*(x,+(y,-(y))),w) -11|[]-> +(*(*(x,y),w),*(*(x,-(y)),w)) 0() <-4|[]- +(+(x,y),-(+(x,y))) -12|[]-> +(x,+(y,-(+(x,y)))) +(0(),z) <-4|0[]- +(+(x,-(x)),z) -12|[]-> +(x,+(-(x),z)) +(x,0()) <-4|1[]- +(x,+(y,-(y))) -13|[]-> +(+(x,y),-(y)) 0() <-4|[]- +(x,-(x)) -14|[]-> +(-(x),x) 0() <-5|[]- +(+(x1405,-(x1405)),0()) -0|[]-> +(x1405,-(x1405)) -(y) <-5|0[]- -(+(+(x1407,-(x1407)),y)) -3|[]-> +(-(+(x1407,-(x1407))),-(y)) -(+(x1409,-(x1409))) <-5|[]- +(+(x1409,-(x1409)),-(+(x1409,-(x1409)))) -4|[]-> 0() +(-(+(x1411,-(x1411))),y) <-5|0[]- +(+(+(x1411,-(x1411)),-(+(x1411,-(x1411)))),y) -5|[]-> y *(x,z) <-5|1[]- *(x,+(+(x1413,-(x1413)),z)) -10|[]-> +(*(x,+(x1413,-(x1413))),*(x,z)) *(*(x,z),w) <-5|0,1[]- *(*(x,+(+(x1415,-(x1415)),z)),w) -11|[]-> + ( *(*(x,+(x1415,-(x1415))),w), * (*(x,z),w)) z <-5|[]- +(+(x,-(x)),z) -12|[]-> +(x,+(-(x),z)) +(y,z) <-5|0[]- +(+(+(x1419,-(x1419)),y),z) -12|[]-> +(+(x1419,-(x1419)),+(y,z)) +(y,z) <-5|[]- +(+(x1421,-(x1421)),+(y,z)) -13|[]-> +(+(+(x1421,-(x1421)),y),z) +(x,z) <-5|1[]- +(x,+(+(x1423,-(x1423)),z)) -13|[]-> +(+(x,+(x1423,-(x1423))),z) y <-5|[]- +(+(x1425,-(x1425)),y) -14|[]-> +(y,+(x1425,-(x1425))) 0() <-6|[]- *(*(x,-(y)),0()) -9|[]-> *(-(*(x,y)),0()) 0() <-6|[]- *(*(x,+(y,z)),0()) -11|[]-> +(*(*(x,y),0()),*(*(x,z),0())) 0() <-6|[]- *(*(x,y),0()) -15|[]-> *(x,*(y,0())) *(0(),z) <-6|0[]- *(*(x,0()),z) -15|[]-> *(x,*(0(),z)) *(x,0()) <-6|1[]- *(x,*(y,0())) -16|[]-> *(*(x,y),0()) 0() <-6|[]- *(x,0()) -17|[]-> *(0(),x) *(x,-(y)) <-7|[]- *(*(x,-(y)),1()) -9|[]-> *(-(*(x,y)),1()) *(x,+(y,z)) <-7|[]- *(*(x,+(y,z)),1()) -11|[]-> +(*(*(x,y),1()),*(*(x,z),1())) *(x,y) <-7|[]- *(*(x,y),1()) -15|[]-> *(x,*(y,1())) *(x,z) <-7|0[]- *(*(x,1()),z) -15|[]-> *(x,*(1(),z)) *(x,y) <-7|1[]- *(x,*(y,1())) -16|[]-> *(*(x,y),1()) x <-7|[]- *(x,1()) -17|[]-> *(1(),x) -(*(*(x,-(y)),x1440)) <-8|[]- *(*(x,-(y)),-(x1440)) -9|[]-> *(-(*(x,y)),-(x1440)) *(-(*(x,y)),z) <-8|0[]- *(*(x,-(y)),z) -9|[]-> *(-(*(x,y)),z) -(*(*(x,+(y,z)),x1444)) <-8|[]- *(*(x,+(y,z)),-(x1444)) -11|[]-> + ( *(*(x,y),-(x1444)), * (*(x,z),-(x1444))) -(*(*(x,y),x1446)) <-8|[]- *(*(x,y),-(x1446)) -15|[]-> *(x,*(y,-(x1446))) *(-(*(x,x1448)),z) <-8|0[]- *(*(x,-(x1448)),z) -15|[]-> *(x,*(-(x1448),z)) *(x,-(*(y,x1450))) <-8|1[]- *(x,*(y,-(x1450))) -16|[]-> *(*(x,y),-(x1450)) -(*(x,x1452)) <-8|[]- *(x,-(x1452)) -17|[]-> *(-(x1452),x) *(-(*(x1453,x1454)),0()) <-9|[]- *(*(x1453,-(x1454)),0()) -6|[]-> 0() *(-(*(x1456,x1457)),1()) <-9|[]- *(*(x1456,-(x1457)),1()) -7|[]-> *(x1456,-(x1457)) *(-(*(x1459,x1460)),-(y)) <-9|[]- *(*(x1459,-(x1460)),-(y)) -8|[]-> -(*(*(x1459,-(x1460)),y)) *(*(-(*(x1462,x1463)),-(y)),z) <-9|0[]- *(*(*(x1462,-(x1463)),-(y)),z) -9| []-> *(-(*(*(x1462,-(x1463)),y)),z) *(-(*(x1465,x1466)),+(y,z)) <-9|[]- *(*(x1465,-(x1466)),+(y,z)) -10| []-> +(*(*(x1465,-(x1466)),y),*(*(x1465,-(x1466)),z)) *(*(-(*(x1468,x1469)),+(y,z)),w) <-9|0[]- *(*(*(x1468,-(x1469)),+(y,z)),w) -11| []-> +(*(*(*(x1468,-(x1469)),y),w), *(*(*(x1468,-(x1469)),z),w)) *(-(*(x,x1472)),z) <-9|[]- *(*(x,-(x1472)),z) -15|[]-> *(x,*(-(x1472),z)) *(*(-(*(x1474,x1475)),y),z) <-9|0[]- *(*(*(x1474,-(x1475)),y),z) -15| []-> *(*(x1474,-(x1475)),*(y,z)) *(-(*(x1477,x1478)),*(y,z)) <-9|[]- *(*(x1477,-(x1478)),*(y,z)) -16| []-> *(*(*(x1477,-(x1478)),y),z) *(x,*(-(*(x1480,x1481)),z)) <-9|1[]- *(x,*(*(x1480,-(x1481)),z)) -16| []-> *(*(x,*(x1480,-(x1481))),z) *(-(*(x1483,x1484)),y) <-9|[]- *(*(x1483,-(x1484)),y) -17|[]-> *(y,*(x1483,-(x1484))) +(*(*(x,-(y)),x1487),*(*(x,-(y)),x1488)) <-10|[]- *(*(x,-(y)),+(x1487,x1488)) -9| []-> *(-(*(x,y)),+(x1487,x1488)) +(*(*(x,+(y,z)),x1490),*(*(x,+(y,z)),x1491)) <-10|[]- *(*(x,+(y,z)),+(x1490,x1491)) -11| []-> +(*(*(x,y),+(x1490,x1491)), *(*(x,z),+(x1490,x1491))) *(+(*(x,y),*(x,z)),w) <-10|0[]- *(*(x,+(y,z)),w) -11|[]-> +(*(*(x,y),w),*(*(x,z),w)) +(*(*(x,y),x1496),*(*(x,y),x1497)) <-10|[]- *(*(x,y),+(x1496,x1497)) -15| []-> *(x,*(y,+(x1496,x1497))) *(+(*(x,x1499),*(x,x1500)),z) <-10|0[]- *(*(x,+(x1499,x1500)),z) -15| []-> *(x,*(+(x1499,x1500),z)) *(x,+(*(y,x1502),*(y,x1503))) <-10|1[]- *(x,*(y,+(x1502,x1503))) -16| []-> *(*(x,y),+(x1502,x1503)) +(*(x,x1505),*(x,x1506)) <-10|[]- *(x,+(x1505,x1506)) -17|[]-> *(+(x1505,x1506),x) +(*(*(x1507,x1508),0()),*(*(x1507,x1509),0())) <-11|[]- *(*(x1507,+(x1508,x1509)),0()) -6| []-> 0() +(*(*(x1511,x1512),1()),*(*(x1511,x1513),1())) <-11|[]- *(*(x1511,+(x1512,x1513)),1()) -7| []-> *(x1511,+(x1512,x1513)) +(*(*(x1515,x1516),-(y)),*(*(x1515,x1517),-(y))) <-11|[]- *(*(x1515,+(x1516,x1517)),-(y)) -8| []-> -(*(*(x1515,+(x1516,x1517)),y)) *(+(*(*(x1519,x1520),-(y)),*(*(x1519,x1521),-(y))),z) <-11|0[]- *( *(*(x1519,+(x1520,x1521)),-(y)), z) -9| []-> *( -(*(*(x1519,+(x1520,x1521)),y)), z) +(*(*(x1523,x1524),+(y,z)),*(*(x1523,x1525),+(y,z))) <-11|[]- *(*(x1523,+(x1524,x1525)),+(y,z)) -10| []-> +(*(*(x1523,+(x1524,x1525)),y), *(*(x1523,+(x1524,x1525)),z)) *(+(*(*(x1527,x1528),+(y,z)),*(*(x1527,x1529),+(y,z))),w) <-11|0[]- *(*(*(x1527,+(x1528,x1529)),+(y,z)),w) -11|[]-> +(*(*(*(x1527,+(x1528,x1529)),y),w), *(*(*(x1527,+(x1528,x1529)),z),w)) +(*(*(x,x1532),z),*(*(x,x1533),z)) <-11|[]- *(*(x,+(x1532,x1533)),z) -15| []-> *(x,*(+(x1532,x1533),z)) *(+(*(*(x1535,x1536),y),*(*(x1535,x1537),y)),z) <-11|0[]- *(*(*(x1535,+(x1536,x1537)),y),z) -15| []-> *(*(x1535,+(x1536,x1537)),*(y,z)) +(*(*(x1539,x1540),*(y,z)),*(*(x1539,x1541),*(y,z))) <-11|[]- *(*(x1539,+(x1540,x1541)),*(y,z)) -16| []-> *(*(*(x1539,+(x1540,x1541)),y),z) *(x,+(*(*(x1543,x1544),z),*(*(x1543,x1545),z))) <-11|1[]- *(x,*(*(x1543,+(x1544,x1545)),z)) -16| []-> *(*(x,*(x1543,+(x1544,x1545))),z) +(*(*(x1547,x1548),y),*(*(x1547,x1549),y)) <-11|[]- *(*(x1547,+(x1548,x1549)),y) -17| []-> *(y,*(x1547,+(x1548,x1549))) +(x1551,+(x1552,0())) <-12|[]- +(+(x1551,x1552),0()) -0|[]-> +(x1551,x1552) -(+(x1554,+(x1555,y))) <-12|0[]- -(+(+(x1554,x1555),y)) -3|[]-> +(-(+(x1554,x1555)),-(y)) +(x1557,+(x1558,-(+(x1557,x1558)))) <-12|[]- +(+(x1557,x1558),-(+(x1557,x1558))) -4|[]-> 0() +(x,+(-(x),y)) <-12|[]- +(+(x,-(x)),y) -5|[]-> y +(+(x1563,+(x1564,-(+(x1563,x1564)))),y) <-12|0[]- +(+(+(x1563,x1564),-(+(x1563,x1564))),y) -5| []-> y *(x,+(x1566,+(x1567,z))) <-12|1[]- *(x,+(+(x1566,x1567),z)) -10|[]-> +(*(x,+(x1566,x1567)),*(x,z)) *(*(x,+(x1569,+(x1570,z))),w) <-12|0,1[]- *(*(x,+(+(x1569,x1570),z)),w) -11| []-> +(*(*(x,+(x1569,x1570)),w),*(*(x,z),w)) +(+(x1572,+(x1573,y)),z) <-12|0[]- +(+(+(x1572,x1573),y),z) -12|[]-> +(+(x1572,x1573),+(y,z)) +(x1575,+(x1576,+(y,z))) <-12|[]- +(+(x1575,x1576),+(y,z)) -13|[]-> +(+(+(x1575,x1576),y),z) +(x,+(x1578,+(x1579,z))) <-12|1[]- +(x,+(+(x1578,x1579),z)) -13|[]-> +(+(x,+(x1578,x1579)),z) +(x1581,+(x1582,y)) <-12|[]- +(+(x1581,x1582),y) -14|[]-> +(y,+(x1581,x1582)) -(+(+(x,x1585),x1586)) <-13|0[]- -(+(x,+(x1585,x1586))) -3|[]-> +(-(x),-(+(x1585,x1586))) +(+(+(x,-(x)),x1588),x1589) <-13|[]- +(+(x,-(x)),+(x1588,x1589)) -5|[]-> +(x1588,x1589) *(x,+(+(y,x1591),x1592)) <-13|1[]- *(x,+(y,+(x1591,x1592))) -10|[]-> +(*(x,y),*(x,+(x1591,x1592))) *(*(x,+(+(y,x1594),x1595)),w) <-13|0,1[]- *(*(x,+(y,+(x1594,x1595))),w) -11| []-> +(*(*(x,y),w),*(*(x,+(x1594,x1595)),w)) +(+(+(x,y),x1597),x1598) <-13|[]- +(+(x,y),+(x1597,x1598)) -12|[]-> +(x,+(y,+(x1597,x1598))) +(+(+(x,x1600),x1601),z) <-13|0[]- +(+(x,+(x1600,x1601)),z) -12|[]-> +(x,+(+(x1600,x1601),z)) +(x,+(+(y,x1603),x1604)) <-13|1[]- +(x,+(y,+(x1603,x1604))) -13|[]-> +(+(x,y),+(x1603,x1604)) +(+(x,x1606),x1607) <-13|[]- +(x,+(x1606,x1607)) -14|[]-> +(+(x1606,x1607),x) +(0(),x) <-14|[]- +(x,0()) -0|[]-> x -(+(y,x)) <-14|0[]- -(+(x,y)) -3|[]-> +(-(x),-(y)) +(-(x),x) <-14|[]- +(x,-(x)) -4|[]-> 0() +(y,+(x,-(x))) <-14|[]- +(+(x,-(x)),y) -5|[]-> y +(+(-(x),x),y) <-14|0[]- +(+(x,-(x)),y) -5|[]-> y *(x,+(z,y)) <-14|1[]- *(x,+(y,z)) -10|[]-> +(*(x,y),*(x,z)) *(*(x,+(z,y)),w) <-14|0,1[]- *(*(x,+(y,z)),w) -11|[]-> +(*(*(x,y),w),*(*(x,z),w)) +(z,+(x,y)) <-14|[]- +(+(x,y),z) -12|[]-> +(x,+(y,z)) +(+(y,x),z) <-14|0[]- +(+(x,y),z) -12|[]-> +(x,+(y,z)) +(+(y,z),x) <-14|[]- +(x,+(y,z)) -13|[]-> +(+(x,y),z) +(x,+(z,y)) <-14|1[]- +(x,+(y,z)) -13|[]-> +(+(x,y),z) *(x1630,*(x1631,0())) <-15|[]- *(*(x1630,x1631),0()) -6|[]-> 0() *(x1633,*(x1634,1())) <-15|[]- *(*(x1633,x1634),1()) -7|[]-> *(x1633,x1634) *(x1636,*(x1637,-(y))) <-15|[]- *(*(x1636,x1637),-(y)) -8|[]-> -(*(*(x1636,x1637),y)) *(x,*(-(y),z)) <-15|[]- *(*(x,-(y)),z) -9|[]-> *(-(*(x,y)),z) *(*(x1642,*(x1643,-(y))),z) <-15|0[]- *(*(*(x1642,x1643),-(y)),z) -9| []-> *(-(*(*(x1642,x1643),y)),z) *(x1645,*(x1646,+(y,z))) <-15|[]- *(*(x1645,x1646),+(y,z)) -10|[]-> +(*(*(x1645,x1646),y),*(*(x1645,x1646),z)) *(x,*(+(y,z),w)) <-15|[]- *(*(x,+(y,z)),w) -11|[]-> +(*(*(x,y),w),*(*(x,z),w)) *(*(x1651,*(x1652,+(y,z))),w) <-15|0[]- *(*(*(x1651,x1652),+(y,z)),w) -11| []-> +(*(*(*(x1651,x1652),y),w),*(*(*(x1651,x1652),z),w)) *(*(x1654,*(x1655,y)),z) <-15|0[]- *(*(*(x1654,x1655),y),z) -15|[]-> *(*(x1654,x1655),*(y,z)) *(x1657,*(x1658,*(y,z))) <-15|[]- *(*(x1657,x1658),*(y,z)) -16|[]-> *(*(*(x1657,x1658),y),z) *(x,*(x1660,*(x1661,z))) <-15|1[]- *(x,*(*(x1660,x1661),z)) -16|[]-> *(*(x,*(x1660,x1661)),z) *(x1663,*(x1664,y)) <-15|[]- *(*(x1663,x1664),y) -17|[]-> *(y,*(x1663,x1664)) *(*(*(x,-(y)),x1667),x1668) <-16|[]- *(*(x,-(y)),*(x1667,x1668)) -9| []-> *(-(*(x,y)),*(x1667,x1668)) *(*(*(x,+(y,z)),x1670),x1671) <-16|[]- *(*(x,+(y,z)),*(x1670,x1671)) -11| []-> +(*(*(x,y),*(x1670,x1671)),*(*(x,z),*(x1670,x1671))) *(*(*(x,y),x1673),x1674) <-16|[]- *(*(x,y),*(x1673,x1674)) -15|[]-> *(x,*(y,*(x1673,x1674))) *(*(*(x,x1676),x1677),z) <-16|0[]- *(*(x,*(x1676,x1677)),z) -15|[]-> *(x,*(*(x1676,x1677),z)) *(x,*(*(y,x1679),x1680)) <-16|1[]- *(x,*(y,*(x1679,x1680))) -16|[]-> *(*(x,y),*(x1679,x1680)) *(*(x,x1682),x1683) <-16|[]- *(x,*(x1682,x1683)) -17|[]-> *(*(x1682,x1683),x) *(0(),x) <-17|[]- *(x,0()) -6|[]-> 0() *(1(),x) <-17|[]- *(x,1()) -7|[]-> x *(-(y),x) <-17|[]- *(x,-(y)) -8|[]-> -(*(x,y)) *(z,*(x,-(y))) <-17|[]- *(*(x,-(y)),z) -9|[]-> *(-(*(x,y)),z) *(*(-(y),x),z) <-17|0[]- *(*(x,-(y)),z) -9|[]-> *(-(*(x,y)),z) *(+(y,z),x) <-17|[]- *(x,+(y,z)) -10|[]-> +(*(x,y),*(x,z)) *(w,*(x,+(y,z))) <-17|[]- *(*(x,+(y,z)),w) -11|[]-> +(*(*(x,y),w),*(*(x,z),w)) *(*(+(y,z),x),w) <-17|0[]- *(*(x,+(y,z)),w) -11|[]-> +(*(*(x,y),w),*(*(x,z),w)) *(z,*(x,y)) <-17|[]- *(*(x,y),z) -15|[]-> *(x,*(y,z)) *(*(y,x),z) <-17|0[]- *(*(x,y),z) -15|[]-> *(x,*(y,z)) *(*(y,z),x) <-17|[]- *(x,*(y,z)) -16|[]-> *(*(x,y),z) *(x,*(z,y)) <-17|1[]- *(x,*(y,z)) -16|[]-> *(*(x,y),z) Redundant Rules Transformation: +(x,0()) -> x -(0()) -> 0() -(-(x)) -> x -(+(x,y)) -> +(-(x),-(y)) +(x,-(x)) -> 0() *(x,0()) -> 0() *(x,1()) -> x *(x,-(y)) -> -(*(x,y)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) *(x,*(y,z)) -> *(*(x,y),z) *(x,y) -> *(y,x) Church Rosser Transformation Processor (ac): f6_AC(x,0()) -> x -(0()) -> 0() -(-(x)) -> x -(f6_AC(x,y)) -> f6_AC(-(x),-(y)) f6_AC(x,-(x)) -> 0() f8_AC(x,0()) -> 0() f8_AC(x,1()) -> x f8_AC(x,-(y)) -> -(f8_AC(x,y)) f8_AC(x,f6_AC(y,z)) -> f6_AC(f8_AC(x,y),f8_AC(x,z)) AC critical peaks: joinable AC-RPO Processor: precedence: 1 > f8_AC > - > 0 > f6_AC status: problem: Qed