(ignored inputs)COMMENT Theory of Distributive Lattice from [PS81]. Remark that a typo has been reported. In rule 2 "joint" should have been "join" . See "108.trs" .
Rewrite Rules:
[ join(?x,meet(?x,?y)) -> ?x,
meet(?x,joint(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)),
meet(?x,?x) -> ?x,
join(?x,?x) -> ?x,
meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)),
meet(?x,?y) -> meet(?y,?x),
join(join(?x,?y),?z) -> join(?x,join(?y,?z)),
join(?x,?y) -> join(?y,?x) ]
Apply Direct Methods...
Inner CPs:
[ join(?x_1,join(meet(?x_1,?y_1),meet(?x_1,?z_1))) = ?x_1,
join(?x_2,?x_2) = ?x_2,
join(meet(?x_4,?y_4),meet(?x_4,meet(?y_4,?z_4))) = meet(?x_4,?y_4),
join(?x_5,meet(?y_5,?x_5)) = ?x_5,
meet(join(meet(?x_1,?y_1),meet(?x_1,?z_1)),?z_4) = meet(?x_1,meet(joint(?y_1,?z_1),?z_4)),
meet(?x_2,?z_4) = meet(?x_2,meet(?x_2,?z_4)),
meet(meet(?y_5,?x_5),?z_4) = meet(?x_5,meet(?y_5,?z_4)),
join(?x,?z_6) = join(?x,join(meet(?x,?y),?z_6)),
join(?x_3,?z_6) = join(?x_3,join(?x_3,?z_6)),
join(join(?y_7,?x_7),?z_6) = join(?x_7,join(?y_7,?z_6)),
meet(meet(?x,meet(?y,?z)),?z_1) = meet(meet(?x,?y),meet(?z,?z_1)),
join(join(?x,join(?y,?z)),?z_1) = join(join(?x,?y),join(?z,?z_1)) ]
Outer CPs:
[ join(?x_6,?y_6) = join(?x_6,join(?y_6,meet(join(?x_6,?y_6),?y))),
?x = join(meet(?x,?y),?x),
join(meet(joint(?y_1,?z_1),?y_1),meet(joint(?y_1,?z_1),?z_1)) = joint(?y_1,?z_1),
join(meet(meet(?x_4,?y_4),?y_1),meet(meet(?x_4,?y_4),?z_1)) = meet(?x_4,meet(?y_4,joint(?y_1,?z_1))),
join(meet(?x_1,?y_1),meet(?x_1,?z_1)) = meet(joint(?y_1,?z_1),?x_1),
meet(?x_4,?y_4) = meet(?x_4,meet(?y_4,meet(?x_4,?y_4))),
?x_2 = meet(?x_2,?x_2),
join(?x_6,?y_6) = join(?x_6,join(?y_6,join(?x_6,?y_6))),
?x_3 = join(?x_3,?x_3),
meet(?x_4,meet(?y_4,?z_4)) = meet(?z_4,meet(?x_4,?y_4)),
join(?x_6,join(?y_6,?z_6)) = join(?z_6,join(?x_6,?y_6)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
not Left-Linear, not Right-Linear
unknown Strongly Depth-Preserving & Non-E-Overlapping
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
[ join(?x,meet(?x,?y)) -> ?x,
meet(?x,joint(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)),
meet(?x,?x) -> ?x,
join(?x,?x) -> ?x ]
P:
[ meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)),
meet(?x,?y) -> meet(?y,?x),
join(join(?x,?y),?z) -> join(?x,join(?y,?z)),
join(?x,?y) -> join(?y,?x) ]
S: not left-linear
failure(Step 1)
STEP: 2 (linear)
S:
[ join(?x,meet(?x,?y)) -> ?x,
meet(?x,joint(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)),
meet(?x,?x) -> ?x,
join(?x,?x) -> ?x ]
P:
[ meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)),
meet(?x,?y) -> meet(?y,?x),
join(join(?x,?y),?z) -> join(?x,join(?y,?z)),
join(?x,?y) -> join(?y,?x) ]
S: not linear
failure(Step 2)
STEP: 3 (relative)
S:
[ join(?x,meet(?x,?y)) -> ?x,
meet(?x,joint(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)),
meet(?x,?x) -> ?x,
join(?x,?x) -> ?x ]
P:
[ meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)),
meet(?x,?y) -> meet(?y,?x),
join(join(?x,?y),?z) -> join(?x,join(?y,?z)),
join(?x,?y) -> join(?y,?x) ]
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
check Non-Confluence...Unknown
Direct Methods: Can't judge
Try Persistent Decomposition for...
[ join(?x,meet(?x,?y)) -> ?x,
meet(?x,joint(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)),
meet(?x,?x) -> ?x,
join(?x,?x) -> ?x,
meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)),
meet(?x,?y) -> meet(?y,?x),
join(join(?x,?y),?z) -> join(?x,join(?y,?z)),
join(?x,?y) -> join(?y,?x) ]
Sort Assignment:
join : 27*27=>27
meet : 27*27=>27
joint : 27*27=>27
maximal types: {27}
Persistent Decomposition failed: Can't judge
Try Layer Preserving Decomposition for...
[ join(?x,meet(?x,?y)) -> ?x,
meet(?x,joint(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)),
meet(?x,?x) -> ?x,
join(?x,?x) -> ?x,
meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)),
meet(?x,?y) -> meet(?y,?x),
join(join(?x,?y),?z) -> join(?x,join(?y,?z)),
join(?x,?y) -> join(?y,?x) ]
Layer Preserving Decomposition failed: Can't judge
Try Commutative Decomposition for...
[ join(?x,meet(?x,?y)) -> ?x,
meet(?x,joint(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)),
meet(?x,?x) -> ?x,
join(?x,?x) -> ?x,
meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)),
meet(?x,?y) -> meet(?y,?x),
join(join(?x,?y),?z) -> join(?x,join(?y,?z)),
join(?x,?y) -> join(?y,?x) ]
Commutative Decomposition failed (not left-linear): Can't judge
No further decomposition possible
Final result: Can't judge
/local-scratch/hzankl/2012/cops2012/78.trs: Failure(unknown)
(258 msec.)