(COMMENT generated from Maude module 'RENAMED-BOOL' by 'complete' transformation)
(VAR A B C U' U V1 V2 X Z Y)
(THEORY (AC _xor_)
(AC _or_)
(AC _and_))
(RULES
U101(tt,A,B) -> _xor_(_and_(A,B),_xor_(A,B))

U11(tt,A) -> A

U111(tt) -> false

U121(tt,A) -> A

U131(tt,B,U') -> U132(equal(_isNotEqualTo_(B,true),true),U')

U132(tt,U') -> U'

U141(tt,U) -> U

U151(tt,V1,V2) -> U152(isBool(V1),V2)

U152(tt,V2) -> U153(isBool(V2))

U153(tt) -> tt

U161(tt,V1,V2) -> U162(isBool(V1),V2)

U162(tt,V2) -> U163(isBool(V2))

U163(tt) -> tt

U171(tt,V1,V2) -> U172(isBool(V1),V2)

U172(tt,V2) -> U173(isBool(V2))

U173(tt) -> tt

U181(tt,V1,V2) -> U182(isBool(V1),V2)

U182(tt,V2) -> U183(isBool(V2))

U183(tt) -> tt

U191(tt,V1) -> U192(isBool(V1))

U192(tt) -> tt

U201(tt,A) -> _xor_(A,true)

U21(tt,A,B,C) -> _xor_(_and_(A,B),_and_(A,C))

U31(tt) -> false

U41(tt,A) -> A

U51(tt,A,B) -> not_(_xor_(A,_and_(A,B)))

U61(tt,U',U) -> U62(equal(_isNotEqualTo_(U,U'),true))

U62(tt) -> false

U71(tt) -> true

U81(tt,U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false,true)

U91(tt) -> false

_and_(A,A) -> U11(and(isBool(A),isBoolKind(A)),A)

_and_(A,_xor_(B,C)) -> U21(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C)))),A,B,C)

_and_(false,A) -> U31(and(isBool(A),isBoolKind(A)))

_and_(true,A) -> U41(and(isBool(A),isBoolKind(A)),A)

_implies_(A,B) -> U51(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B)

_isEqualTo_(U,U') -> U61(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U)

_isEqualTo_(U,U) -> U71(and(isS(U),isSKind(U)))

_isNotEqualTo_(U,U') -> U81(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U)

_isNotEqualTo_(U,U) -> U91(and(isS(U),isSKind(U)))

_or_(A,B) -> U101(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B)

_xor_(A,A) -> U111(and(isBool(A),isBoolKind(A)))

_xor_(false,A) -> U121(and(isBool(A),isBoolKind(A)),A)

and(tt,X) -> X

equal(X,X) -> tt

if_then_else_fi(B,U,U') -> U131(and(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))),B,U')

if_then_else_fi(true,U,U') -> U141(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U)

isBool(false) -> tt

isBool(true) -> tt

isBool(_and_(V1,V2)) -> U151(and(isBoolKind(V1),isBoolKind(V2)),V1,V2)

isBool(_implies_(V1,V2)) -> U161(and(isBoolKind(V1),isBoolKind(V2)),V1,V2)

isBool(_isEqualTo_(V1,V2)) -> tt

isBool(_isNotEqualTo_(V1,V2)) -> tt

isBool(_or_(V1,V2)) -> U171(and(isBoolKind(V1),isBoolKind(V2)),V1,V2)

isBool(_xor_(V1,V2)) -> U181(and(isBoolKind(V1),isBoolKind(V2)),V1,V2)

isBool(not_(V1)) -> U191(isBoolKind(V1),V1)

isBoolKind(false) -> tt

isBoolKind(true) -> tt

isBoolKind(_and_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2))

isBoolKind(_implies_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2))

isBoolKind(_isEqualTo_(V1,V2)) -> tt

isBoolKind(_isNotEqualTo_(V1,V2)) -> tt

isBoolKind(_or_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2))

isBoolKind(_xor_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2))

isBoolKind(not_(V1)) -> isBoolKind(V1)

not_(A) -> U201(and(isBool(A),isBoolKind(A)),A)

not_(false) -> true

not_(true) -> false
)