MAYBE Time: 0.041884 TRS: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} DP: DP: { sent# up x -> sent# x, rec# sent x -> sent# rec x, rec# sent x -> rec# x, rec# rec x -> sent# rec x, rec# no x -> sent# rec x, rec# no x -> rec# x, rec# up x -> rec# x, rec# bot() -> sent# bot(), no# up x -> no# x, top# sent up x -> rec# x, top# sent up x -> top# check rec x, top# sent up x -> check# rec x, top# rec up x -> rec# x, top# rec up x -> top# check rec x, top# rec up x -> check# rec x, top# no up x -> rec# x, top# no up x -> top# check rec x, top# no up x -> check# rec x, check# sent x -> sent# check x, check# sent x -> check# x, check# rec x -> rec# check x, check# rec x -> check# x, check# no x -> no# check x, check# no x -> check# x, check# up x -> check# x} TRS: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} EDG: {(sent# up x -> sent# x, sent# up x -> sent# x) (rec# no x -> rec# x, rec# bot() -> sent# bot()) (rec# no x -> rec# x, rec# up x -> rec# x) (rec# no x -> rec# x, rec# no x -> rec# x) (rec# no x -> rec# x, rec# no x -> sent# rec x) (rec# no x -> rec# x, rec# rec x -> sent# rec x) (rec# no x -> rec# x, rec# sent x -> rec# x) (rec# no x -> rec# x, rec# sent x -> sent# rec x) (no# up x -> no# x, no# up x -> no# x) (top# rec up x -> rec# x, rec# bot() -> sent# bot()) (top# rec up x -> rec# x, rec# up x -> rec# x) (top# rec up x -> rec# x, rec# no x -> rec# x) (top# rec up x -> rec# x, rec# no x -> sent# rec x) (top# rec up x -> rec# x, rec# rec x -> sent# rec x) (top# rec up x -> rec# x, rec# sent x -> rec# x) (top# rec up x -> rec# x, rec# sent x -> sent# rec x) (check# sent x -> check# x, check# up x -> check# x) (check# sent x -> check# x, check# no x -> check# x) (check# sent x -> check# x, check# no x -> no# check x) (check# sent x -> check# x, check# rec x -> check# x) (check# sent x -> check# x, check# rec x -> rec# check x) (check# sent x -> check# x, check# sent x -> check# x) (check# sent x -> check# x, check# sent x -> sent# check x) (check# no x -> check# x, check# up x -> check# x) (check# no x -> check# x, check# no x -> check# x) (check# no x -> check# x, check# no x -> no# check x) (check# no x -> check# x, check# rec x -> check# x) (check# no x -> check# x, check# rec x -> rec# check x) (check# no x -> check# x, check# sent x -> check# x) (check# no x -> check# x, check# sent x -> sent# check x) (top# sent up x -> top# check rec x, top# no up x -> check# rec x) (top# sent up x -> top# check rec x, top# no up x -> top# check rec x) (top# sent up x -> top# check rec x, top# no up x -> rec# x) (top# sent up x -> top# check rec x, top# rec up x -> check# rec x) (top# sent up x -> top# check rec x, top# rec up x -> top# check rec x) (top# sent up x -> top# check rec x, top# rec up x -> rec# x) (top# sent up x -> top# check rec x, top# sent up x -> check# rec x) (top# sent up x -> top# check rec x, top# sent up x -> top# check rec x) (top# sent up x -> top# check rec x, top# sent up x -> rec# x) (top# no up x -> top# check rec x, top# no up x -> check# rec x) (top# no up x -> top# check rec x, top# no up x -> top# check rec x) (top# no up x -> top# check rec x, top# no up x -> rec# x) (top# no up x -> top# check rec x, top# rec up x -> check# rec x) (top# no up x -> top# check rec x, top# rec up x -> top# check rec x) (top# no up x -> top# check rec x, top# rec up x -> rec# x) (top# no up x -> top# check rec x, top# sent up x -> check# rec x) (top# no up x -> top# check rec x, top# sent up x -> top# check rec x) (top# no up x -> top# check rec x, top# sent up x -> rec# x) (rec# rec x -> sent# rec x, sent# up x -> sent# x) (top# sent up x -> check# rec x, check# up x -> check# x) (top# sent up x -> check# rec x, check# no x -> check# x) (top# sent up x -> check# rec x, check# no x -> no# check x) (top# sent up x -> check# rec x, check# rec x -> check# x) (top# sent up x -> check# rec x, check# rec x -> rec# check x) (top# sent up x -> check# rec x, check# sent x -> check# x) (top# sent up x -> check# rec x, check# sent x -> sent# check x) (top# no up x -> check# rec x, check# up x -> check# x) (top# no up x -> check# rec x, check# no x -> check# x) (top# no up x -> check# rec x, check# no x -> no# check x) (top# no up x -> check# rec x, check# rec x -> check# x) (top# no up x -> check# rec x, check# rec x -> rec# check x) (top# no up x -> check# rec x, check# sent x -> check# x) (top# no up x -> check# rec x, check# sent x -> sent# check x) (check# rec x -> rec# check x, rec# up x -> rec# x) (check# rec x -> rec# check x, rec# no x -> rec# x) (check# rec x -> rec# check x, rec# no x -> sent# rec x) (check# rec x -> rec# check x, rec# rec x -> sent# rec x) (check# rec x -> rec# check x, rec# sent x -> rec# x) (check# rec x -> rec# check x, rec# sent x -> sent# rec x) (check# no x -> no# check x, no# up x -> no# x) (check# sent x -> sent# check x, sent# up x -> sent# x) (top# rec up x -> check# rec x, check# sent x -> sent# check x) (top# rec up x -> check# rec x, check# sent x -> check# x) (top# rec up x -> check# rec x, check# rec x -> rec# check x) (top# rec up x -> check# rec x, check# rec x -> check# x) (top# rec up x -> check# rec x, check# no x -> no# check x) (top# rec up x -> check# rec x, check# no x -> check# x) (top# rec up x -> check# rec x, check# up x -> check# x) (rec# no x -> sent# rec x, sent# up x -> sent# x) (rec# sent x -> sent# rec x, sent# up x -> sent# x) (top# rec up x -> top# check rec x, top# sent up x -> rec# x) (top# rec up x -> top# check rec x, top# sent up x -> top# check rec x) (top# rec up x -> top# check rec x, top# sent up x -> check# rec x) (top# rec up x -> top# check rec x, top# rec up x -> rec# x) (top# rec up x -> top# check rec x, top# rec up x -> top# check rec x) (top# rec up x -> top# check rec x, top# rec up x -> check# rec x) (top# rec up x -> top# check rec x, top# no up x -> rec# x) (top# rec up x -> top# check rec x, top# no up x -> top# check rec x) (top# rec up x -> top# check rec x, top# no up x -> check# rec x) (check# up x -> check# x, check# sent x -> sent# check x) (check# up x -> check# x, check# sent x -> check# x) (check# up x -> check# x, check# rec x -> rec# check x) (check# up x -> check# x, check# rec x -> check# x) (check# up x -> check# x, check# no x -> no# check x) (check# up x -> check# x, check# no x -> check# x) (check# up x -> check# x, check# up x -> check# x) (check# rec x -> check# x, check# sent x -> sent# check x) (check# rec x -> check# x, check# sent x -> check# x) (check# rec x -> check# x, check# rec x -> rec# check x) (check# rec x -> check# x, check# rec x -> check# x) (check# rec x -> check# x, check# no x -> no# check x) (check# rec x -> check# x, check# no x -> check# x) (check# rec x -> check# x, check# up x -> check# x) (top# no up x -> rec# x, rec# sent x -> sent# rec x) (top# no up x -> rec# x, rec# sent x -> rec# x) (top# no up x -> rec# x, rec# rec x -> sent# rec x) (top# no up x -> rec# x, rec# no x -> sent# rec x) (top# no up x -> rec# x, rec# no x -> rec# x) (top# no up x -> rec# x, rec# up x -> rec# x) (top# no up x -> rec# x, rec# bot() -> sent# bot()) (top# sent up x -> rec# x, rec# sent x -> sent# rec x) (top# sent up x -> rec# x, rec# sent x -> rec# x) (top# sent up x -> rec# x, rec# rec x -> sent# rec x) (top# sent up x -> rec# x, rec# no x -> sent# rec x) (top# sent up x -> rec# x, rec# no x -> rec# x) (top# sent up x -> rec# x, rec# up x -> rec# x) (top# sent up x -> rec# x, rec# bot() -> sent# bot()) (rec# up x -> rec# x, rec# sent x -> sent# rec x) (rec# up x -> rec# x, rec# sent x -> rec# x) (rec# up x -> rec# x, rec# rec x -> sent# rec x) (rec# up x -> rec# x, rec# no x -> sent# rec x) (rec# up x -> rec# x, rec# no x -> rec# x) (rec# up x -> rec# x, rec# up x -> rec# x) (rec# up x -> rec# x, rec# bot() -> sent# bot()) (rec# sent x -> rec# x, rec# sent x -> sent# rec x) (rec# sent x -> rec# x, rec# sent x -> rec# x) (rec# sent x -> rec# x, rec# rec x -> sent# rec x) (rec# sent x -> rec# x, rec# no x -> sent# rec x) (rec# sent x -> rec# x, rec# no x -> rec# x) (rec# sent x -> rec# x, rec# up x -> rec# x) (rec# sent x -> rec# x, rec# bot() -> sent# bot())} SCCS (5): Scc: {check# sent x -> check# x, check# rec x -> check# x, check# no x -> check# x, check# up x -> check# x} Scc: {top# sent up x -> top# check rec x, top# rec up x -> top# check rec x, top# no up x -> top# check rec x} Scc: {no# up x -> no# x} Scc: {rec# sent x -> rec# x, rec# no x -> rec# x, rec# up x -> rec# x} Scc: {sent# up x -> sent# x} SCC (4): Strict: {check# sent x -> check# x, check# rec x -> check# x, check# no x -> check# x, check# up x -> check# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(check#) = 0 Strict: {check# sent x -> check# x, check# rec x -> check# x, check# up x -> check# x} EDG: {(check# rec x -> check# x, check# up x -> check# x) (check# rec x -> check# x, check# rec x -> check# x) (check# rec x -> check# x, check# sent x -> check# x) (check# up x -> check# x, check# sent x -> check# x) (check# up x -> check# x, check# rec x -> check# x) (check# up x -> check# x, check# up x -> check# x) (check# sent x -> check# x, check# sent x -> check# x) (check# sent x -> check# x, check# rec x -> check# x) (check# sent x -> check# x, check# up x -> check# x)} SCCS (1): Scc: {check# sent x -> check# x, check# rec x -> check# x, check# up x -> check# x} SCC (3): Strict: {check# sent x -> check# x, check# rec x -> check# x, check# up x -> check# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(check#) = 0 Strict: {check# sent x -> check# x, check# up x -> check# x} EDG: {(check# up x -> check# x, check# up x -> check# x) (check# up x -> check# x, check# sent x -> check# x) (check# sent x -> check# x, check# sent x -> check# x) (check# sent x -> check# x, check# up x -> check# x)} SCCS (1): Scc: {check# sent x -> check# x, check# up x -> check# x} SCC (2): Strict: {check# sent x -> check# x, check# up x -> check# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(check#) = 0 Strict: {check# up x -> check# x} EDG: {(check# up x -> check# x, check# up x -> check# x)} SCCS (1): Scc: {check# up x -> check# x} SCC (1): Strict: {check# up x -> check# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(check#) = 0 Strict: {} Qed SCC (3): Strict: {top# sent up x -> top# check rec x, top# rec up x -> top# check rec x, top# no up x -> top# check rec x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [sent](x0) = 0, [rec](x0) = 0, [no](x0) = 1, [up](x0) = x0, [top](x0) = 0, [check](x0) = x0, [bot] = 0, [top#](x0) = x0 Strict: top# no up x -> top# check rec x 1 + 0x >= 0 + 0x top# rec up x -> top# check rec x 0 + 0x >= 0 + 0x top# sent up x -> top# check rec x 0 + 0x >= 0 + 0x Weak: EDG: {(top# rec up x -> top# check rec x, top# rec up x -> top# check rec x) (top# rec up x -> top# check rec x, top# sent up x -> top# check rec x) (top# sent up x -> top# check rec x, top# sent up x -> top# check rec x) (top# sent up x -> top# check rec x, top# rec up x -> top# check rec x)} SCCS (1): Scc: {top# sent up x -> top# check rec x, top# rec up x -> top# check rec x} SCC (2): Strict: {top# sent up x -> top# check rec x, top# rec up x -> top# check rec x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [sent](x0) = x0, [rec](x0) = x0 + 1, [no](x0) = x0 + 1, [up](x0) = x0 + 1, [top](x0) = 0, [check](x0) = x0, [bot] = 0, [top#](x0) = x0 Strict: top# rec up x -> top# check rec x 2 + 1x >= 1 + 1x top# sent up x -> top# check rec x 1 + 1x >= 1 + 1x Weak: EDG: {(top# sent up x -> top# check rec x, top# sent up x -> top# check rec x)} SCCS (1): Scc: {top# sent up x -> top# check rec x} SCC (1): Strict: {top# sent up x -> top# check rec x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} Fail SCC (1): Strict: {no# up x -> no# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(no#) = 0 Strict: {} Qed SCC (3): Strict: {rec# sent x -> rec# x, rec# no x -> rec# x, rec# up x -> rec# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(rec#) = 0 Strict: {rec# sent x -> rec# x, rec# up x -> rec# x} EDG: {(rec# up x -> rec# x, rec# up x -> rec# x) (rec# up x -> rec# x, rec# sent x -> rec# x) (rec# sent x -> rec# x, rec# sent x -> rec# x) (rec# sent x -> rec# x, rec# up x -> rec# x)} SCCS (1): Scc: {rec# sent x -> rec# x, rec# up x -> rec# x} SCC (2): Strict: {rec# sent x -> rec# x, rec# up x -> rec# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(rec#) = 0 Strict: {rec# up x -> rec# x} EDG: {(rec# up x -> rec# x, rec# up x -> rec# x)} SCCS (1): Scc: {rec# up x -> rec# x} SCC (1): Strict: {rec# up x -> rec# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(rec#) = 0 Strict: {} Qed SCC (1): Strict: {sent# up x -> sent# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} SPSC: Simple Projection: pi(sent#) = 0 Strict: {} Qed