[Submit a comment] [RTALooP home] [Index] [Previous] [Next]  [Postscript] [PDF] [BibTeX Source] [LaTeX Source] 
Originator: J. Zhang
Date: April 1995
Summary: Is there a convergent extended rewrite system for ternary boolean algebra, in which certain equations hold?
Is there a convergent extended rewrite system for ternary boolean algebra, for which the following permutative equations hold:

Date: Wed Dec 20 17:46:07 MET 2000
The following permutative equations hold for every ternary boolean algebra: f(f(x, y, z), u, x) = f(x, y, f(z, u, x)) f(x, y, z) = f(x, z, y) = f(y, x, z) = f(y, z, x) = f(z, x, y) = f(z, y, x) Consider the following set of axioms: Axiom 1: f(f(x1,x2,x3),x4,f(x1,x2,x5)) = f(x1,x2,f(x3,x4,x5)) Axiom 2: f(x1,x1,x2) = x1 This theorem holds true: Theorem 1: f(f(A,B,C),D,A) = f(A,B,f(C,D,A)) Proof: Lemma 1: z = f(z,x4,z) z = by Axiom 2 RL f(z,z,f(y,x4,x5)) = by Axiom 1 RL f(f(z,z,y),x4,f(z,z,x5)) = by Axiom 2 LR f(z,x4,f(z,z,x5)) = by Axiom 2 LR f(z,x4,z) Theorem 1: f(f(A,B,C),D,A) = f(A,B,f(C,D,A)) f(f(A,B,C),D,A) = by Lemma 1 LR f(f(A,B,C),D,f(A,B,A)) = by Axiom 1 LR f(A,B,f(C,D,A)) Consider the following set of axioms: Axiom 1: x1 = f(x2,x1,x1) Axiom 2: x1 = f(x1,x2,g(x2)) Axiom 3: f(x1,x2,f(x3,x4,x5)) = f(f(x1,x2,x3),x4,f(x1,x2,x5)) This theorem holds true: Theorem 1: f(A,B,C) = f(B,A,C) Proof: Lemma 1: f(f(g(x1),x0,q),x0,x1) = f(g(x1),x0,x1) f(f(g(x1),x0,q),x0,x1) = by Axiom 2 LR f(f(f(g(x1),x0,q),x1,g(x1)),x0,x1) = by Axiom 1 LR f(f(f(g(x1),x0,q),x1,g(x1)),x0,f(f(g(x1),x0,q),x1,x1)) = by Axiom 3 RL f(f(g(x1),x0,q),x1,f(g(x1),x0,x1)) = by Axiom 3 RL f(g(x1),x0,f(q,x1,x1)) = by Axiom 1 RL f(g(x1),x0,x1) Lemma 2: f(g(g(y)),y,q) = g(g(y)) f(g(g(y)),y,q) = by Axiom 2 LR f(f(g(g(y)),y,q),y,g(y)) = by Lemma 1 LR f(g(g(y)),y,g(y)) = by Axiom 2 RL g(g(y)) Lemma 3: g(g(z)) = z g(g(z)) = by Lemma 2 RL f(g(g(z)),z,z) = by Axiom 1 RL z Lemma 4: f(y,y,q) = y f(y,y,q) = by Lemma 3 RL f(g(g(y)),y,q) = by Lemma 2 LR g(g(y)) = by Lemma 3 LR y Lemma 5: f(g(x1),y,x1) = y f(g(x1),y,x1) = by Lemma 1 RL f(f(g(x1),y,y),y,x1) = by Axiom 1 RL f(y,y,x1) = by Lemma 4 LR y Lemma 6: f(v,u,x4) = f(u,x4,v) f(v,u,x4) = by Lemma 5 RL f(v,u,f(g(v),x4,v)) = by Axiom 3 LR f(f(v,u,g(v)),x4,f(v,u,v)) = by Axiom 1 LR f(f(v,u,g(v)),x4,f(f(v,v,v),u,v)) = by Axiom 1 LR f(f(v,u,g(v)),x4,f(f(v,v,v),u,f(v,v,v))) = by Axiom 3 RL f(f(v,u,g(v)),x4,f(v,v,f(v,u,v))) = by Lemma 4 LR f(f(v,u,g(v)),x4,v) = by Lemma 3 RL f(f(g(g(v)),u,g(v)),x4,v) = by Lemma 5 LR f(u,x4,v) Theorem 1: f(A,B,C) = f(B,A,C) f(A,B,C) = by Lemma 6 RL f(C,A,B) = by Lemma 5 RL f(C,A,f(g(A),B,A)) = by Axiom 3 LR f(f(C,A,g(A)),B,f(C,A,A)) = by Axiom 1 RL f(f(C,A,g(A)),B,A) = by Axiom 2 RL f(C,B,A) = by Lemma 6 LR f(B,A,C) Consider the following set of axioms: Axiom 1: x1 = f(x2,x1,x1) Axiom 2: x1 = f(x1,x2,g(x2)) Axiom 3: f(x1,x2,f(x3,x4,x5)) = f(f(x1,x2,x3),x4,f(x1,x2,x5)) This theorem holds true: Theorem 1: f(A,B,C) = f(A,C,B) Proof: Lemma 1: f(v,u,f(g(u),x4,u)) = f(v,x4,u) f(v,u,f(g(u),x4,u)) = by Axiom 3 LR f(f(v,u,g(u)),x4,f(v,u,u)) = by Axiom 1 RL f(f(v,u,g(u)),x4,u) = by Axiom 2 RL f(v,x4,u) Lemma 2: f(f(g(x1),x0,q),x0,x1) = f(g(x1),x0,x1) f(f(g(x1),x0,q),x0,x1) = by Lemma 1 RL f(f(g(x1),x0,q),x1,f(g(x1),x0,x1)) = by Axiom 3 RL f(g(x1),x0,f(q,x1,x1)) = by Axiom 1 RL f(g(x1),x0,x1) Lemma 3: f(g(g(y)),y,q) = g(g(y)) f(g(g(y)),y,q) = by Axiom 2 LR f(f(g(g(y)),y,q),y,g(y)) = by Lemma 2 LR f(g(g(y)),y,g(y)) = by Axiom 2 RL g(g(y)) Lemma 4: g(g(z)) = z g(g(z)) = by Lemma 3 RL f(g(g(z)),z,z) = by Axiom 1 RL z Lemma 5: f(y,y,q) = y f(y,y,q) = by Lemma 4 RL f(g(g(y)),y,q) = by Lemma 3 LR g(g(y)) = by Lemma 4 LR y Lemma 6: f(v,u,x4) = f(v,x4,u) f(v,u,x4) = by Lemma 5 RL f(v,u,f(x4,x4,u)) = by Axiom 1 LR f(v,u,f(f(g(u),x4,x4),x4,u)) = by Lemma 2 LR f(v,u,f(g(u),x4,u)) = by Lemma 1 LR f(v,x4,u) Theorem 1: f(A,B,C) = f(A,C,B) f(A,B,C) = by Lemma 6 LR f(A,C,B)
[Submit a comment] [RTALooP home] [Index] [Previous] [Next]  [Postscript] [PDF] [BibTeX Source] [LaTeX Source] 