0.00/0.01 YES 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 0.00/0.01 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR x y) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (or 1, 2) 0.00/0.01 (true) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 or(true,true) -> true 0.00/0.01 or(x,y) -> or(y,x) 0.00/0.01 ) 0.00/0.01 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 Not CS-TRS Procedure: 0.00/0.01 R is not a CS-TRS 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 Linearity Procedure: 0.00/0.01 Linear? 0.00/0.01 YES 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR x y) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (or 1, 2) 0.00/0.01 (true) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 or(true,true) -> true 0.00/0.01 or(x,y) -> or(y,x) 0.00/0.01 ) 0.00/0.01 0.00/0.01 Linear:YES 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 Huet Levy Procedure: 0.00/0.01 -> Rules: 0.00/0.01 or(true,true) -> true 0.00/0.01 or(x,y) -> or(y,x) 0.00/0.01 -> Vars: 0.00/0.01 x, y 0.00/0.01 0.00/0.01 -> Rlps: 0.00/0.01 (rule: or(true,true) -> true, id: 1, possubterms: or(true,true)->[], true->[1], true->[2]) 0.00/0.01 (rule: or(x,y) -> or(y,x), id: 2, possubterms: or(x,y)->[]) 0.00/0.01 0.00/0.01 -> Unifications: 0.00/0.01 (R2 unifies with R1 at p: [], l: or(x,y), lp: or(x,y), sig: {x -> true,y -> true}, l': or(true,true), r: or(y,x), r': true) 0.00/0.01 0.00/0.01 -> Critical pairs info: 0.00/0.01 => Not trivial, Overlay, Proper, NW0, N1 0.00/0.01 0.00/0.01 -> Problem conclusions: 0.00/0.01 Left linear, Right linear, Linear 0.00/0.01 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal 0.00/0.01 Not Huet-Levy confluent, Not Newman confluent 0.00/0.01 R is a TRS 0.00/0.01 Maybe confluent 0.00/0.01 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR x y) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (or 1, 2) 0.00/0.01 (true) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 or(true,true) -> true 0.00/0.01 or(x,y) -> or(y,x) 0.00/0.01 ) 0.00/0.01 0.00/0.01 Critical Pairs: 0.00/0.01 => Not trivial, Overlay, Proper, NW0, N1 0.00/0.01 Linear:YES 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 Critical Pairs Distributor Processor: 0.00/0.01 0.00/0.01 Problem 1.1: 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR x y) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (or 1, 2) 0.00/0.01 (true) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 or(true,true) -> true 0.00/0.01 or(x,y) -> or(y,x) 0.00/0.01 ) 0.00/0.01 0.00/0.01 Critical Pairs: 0.00/0.01 => Not trivial, Overlay, Proper, NW0, N1 0.00/0.01 Linear:YES 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 Strong Confluence Procedure: 0.00/0.01 -> Rewritings: 0.00/0.01 s: true 0.00/0.01 Nodes: [0] 0.00/0.01 Edges: [] 0.00/0.01 ID: 0 => ('true', D0) 0.00/0.01 t: or(true,true) 0.00/0.01 Nodes: [0,1] 0.00/0.01 Edges: [(0,0),(0,1)] 0.00/0.01 ID: 0 => ('or(true,true)', D0) 0.00/0.01 ID: 1 => ('true', D1, R1, P[], S{}), NR: 'true' 0.00/0.01 SNodesPath1: true 0.00/0.01 TNodesPath1: or(true,true) -> true 0.00/0.01 SNodesPath2: true 0.00/0.01 TNodesPath2: or(true,true) -> true 0.00/0.01 true ->= true *<- or(true,true) 0.00/0.01 or(true,true) ->= true *<- true 0.00/0.01 "Strongly closed critical pair" 0.00/0.01 0.00/0.01 The problem is confluent. 0.00/0.01 EOF