unsignedge(S,T) -> unsignedle(T,S)
unsignedgt(S,T) -> unsignedlt(T,S)
unsignedlt(S,0star) -> bit0
unsignedlt(S,S) -> bit0
add(S,0star) -> S
If(S,Bits(32,0star1),Bits(32,0star)) -> ZeroExt(S,31)
signedrshift(signedrshift(Bits(32,S),Bits(32,const26)),Bits(32,const5)) -> signedrshift(S,Bits(32,const31))
signedrshift(MASK=signedrshift(Bits(32,S),Bits(32,const31)),Bits(32,const5)) -> MASK
or(unsignedrshift(signedrshift(A,Bits(32,const26)),Bits(32,const5)),lshift(MASK=signedrshift(A,Bits(32,const31)),Bits(32,const27))) -> MASK
and(signedrshift(xor(and(xor(MINUS=sub(MAX=signedmax(Bits(32,A),Bits(32,B)),signedmin(A,B)),MAX),BXORA=xor(B,A)),MINUS),Bits(32,const31)),BXORA) -> 0star
invert(invert(S)) -> S
Reverse(Reverse(S)) -> S
xor(S,xor(S,T)) -> T
xor(xor(S,T),xor(S,U)) -> xor(T,U)
xor(S,xor(T,xor(S,U))) -> xor(T,U)
xor(S,xor(T,signedmax(S,T))) -> signedmin(S,T)
xor(S,xor(T,signedmin(S,T))) -> signedmax(S,T)
xor(xor(S,T),signedmax(S,T)) -> signedmin(S,T)
xor(xor(S,T),signedmin(S,T)) -> signedmax(S,T)
xor(xor(S,T),xor(U,signedmin(T,U))) -> xor(S,signedmax(T,U))
xor(xor(S,T),xor(U,signedmax(T,U))) -> xor(S,signedmin(T,U))
xor(S,xor(T,xor(U,signedmin(S,U)))) -> xor(T,signedmax(S,U))
xor(S,xor(T,xor(U,signedmax(S,U)))) -> xor(T,signedmin(S,U))
invert(Bits(32,0star)) -> Bits(32,1star)
invert(Bits(32,1star)) -> Bits(32,0star)
invert(Bits(64,0star)) -> Bits(64,1star)
invert(Bits(64,1star)) -> Bits(64,0star)
or(S,0star) -> S
and(S,C=0star) -> C
and(S,1star) -> S
xor(S,0star) -> S
xor(S,1star) -> invert(S)
equal(S,bit0) -> invert(S)
signedlt(S,S) -> bit0
signedlt(01star,S) -> bit0
signedmin(S,01star) -> S
signedmax(S,C=01star) -> C
signedmin(S,C=10star) -> C
signedmax(S,10star) -> S
If(bit0,S,T) -> T
If(S,bit1,bit0) -> S
If(signedle(S,T),S,T) -> signedmin(S,T)
If(signedlt(S,T),S,T) -> signedmin(S,T)
If(signedle(T,S),S,T) -> signedmax(S,T)
If(signedlt(T,S),S,T) -> signedmax(S,T)
signedmin(invert(S),invert(T)) -> invert(signedmax(S,T))
signedmax(invert(S),invert(T)) -> invert(signedmin(S,T))
signedlt(If(S,1star,0star),0star) -> S
signedrshift(X=If(S,1star,0star),T) -> X
Concat(X=If(S,1star,Bits(8,0star)),X,X,X) -> If(S,1star,0star)
Concat(X=If(S,1star,Bits(8,0star)),X,X,X,X,X,X,X) -> If(S,1star,0star)
Extract(Bits(32,A),31,0) -> A
Extract(Bits(64,A),63,0) -> A
Extract(Concat(Bits(64,A),Bits(64,B),Bits(64,C),Bits(64,D)),255,64) -> Concat(A,B,C)
Extract(Concat(Bits(64,A),Bits(64,B),Bits(64,C)),191,64) -> Concat(A,B)
Extract(Concat(Bits(64,A),Bits(64,B)),127,64) -> A
Extract(Concat(S,Bits(8,A),A,A,A,A,A,A,A),63,0) -> Concat(A,A,A,A,A,A,A,A)
Extract(Concat(S,Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B),127,64) -> Concat(A,A,A,A,A,A,A,A)
Extract(Concat(S,Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B),63,0) -> Concat(B,B,B,B,B,B,B,B)
Extract(Concat(S,Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B,Bits(8,C),C,C,C,C,C,C,C),63,0) -> Concat(C,C,C,C,C,C,C,C)
Extract(Concat(S,Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B,Bits(8,C),C,C,C,C,C,C,C),127,64) -> Concat(B,B,B,B,B,B,B,B)
Extract(Concat(S,Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B,Bits(8,C),C,C,C,C,C,C,C),191,128) -> Concat(A,A,A,A,A,A,A,A)
Extract(Concat(Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B,Bits(8,C),C,C,C,C,C,C,C,Bits(8,D),D,D,D,D,D,D,D),63,0) -> Concat(D,D,D,D,D,D,D,D)
Extract(Concat(Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B,Bits(8,C),C,C,C,C,C,C,C,Bits(8,D),D,D,D,D,D,D,D),127,64) -> Concat(C,C,C,C,C,C,C,C)
Extract(Concat(Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B,Bits(8,C),C,C,C,C,C,C,C,Bits(8,D),D,D,D,D,D,D,D),191,128) -> Concat(B,B,B,B,B,B,B,B)
Extract(Concat(Bits(8,A),A,A,A,A,A,A,A,Bits(8,B),B,B,B,B,B,B,B,Bits(8,C),C,C,C,C,C,C,C,Bits(8,D),D,D,D,D,D,D,D),255,192) -> Concat(A,A,A,A,A,A,A,A)
and(T,If(S,1star,C=0star)) -> If(S,T,C)
and(T,If(S,C=0star,1star)) -> If(S,C,T)
or(If(S,T,0star),If(S,0star,U)) -> If(S,T,U)
Concat(If(S,Extract(Bits(64,T),63,32),Extract(U,63,32)),If(S,Extract(T,31,0),Extract(U,31,0))) -> If(S,T,U)
If(signedlt(Bits(64,T),U),Extract(U,63,32),Extract(T,63,32)) -> Extract(signedmax(T,U),63,32)
If(signedlt(Bits(64,T),U),Extract(U,31,0),Extract(T,31,0)) -> Extract(signedmax(T,U),31,0)
Concat(Extract(Bits(64,T),63,32),Extract(T,31,0)) -> T
Concat(If(S,T,U),If(S,V,W)) -> If(S,Concat(T,V),Concat(U,W))
Concat(Bits(32,01star),Bits(32,1star)) -> 01star
invert(If(S,A=1star,Z=0star)) -> If(S,Z,A)
Extract(If(S,1star,0star),63,32) -> If(S,1star,0star)
Extract(If(S,1star,0star),31,0) -> If(S,1star,0star)
Extract(ZeroExt(Bits(32,S),96),31,0) -> S
Extract(ZeroExt(Bits(32,S),96),63,32) -> 0star
Extract(ZeroExt(Bits(64,S),64),63,0) -> S
Extract(ZeroExt(Bits(64,S),192),63,0) -> S
Extract(ZeroExt(Bits(64,S),64),127,64) -> 0star
Extract(ZeroExt(Bits(64,S),192),127,64) -> 0star
Extract(ZeroExt(Bits(64,S),192),191,128) -> 0star
Extract(ZeroExt(Bits(64,S),192),255,192) -> 0star
Extract(or(S,T),31,0) -> or(Extract(S,31,0),Extract(T,31,0))
Extract(or(S,T),63,32) -> or(Extract(S,63,32),Extract(T,63,32))
Extract(or(S,T),95,64) -> or(Extract(S,95,64),Extract(T,95,64))
Extract(or(S,T),127,96) -> or(Extract(S,127,96),Extract(T,127,96))
Extract(or(S,T),159,128) -> or(Extract(S,159,128),Extract(T,159,128))
Extract(or(S,T),191,160) -> or(Extract(S,191,160),Extract(T,191,160))
Extract(or(S,T),223,192) -> or(Extract(S,223,192),Extract(T,223,192))
Extract(or(S,T),255,224) -> or(Extract(S,255,224),Extract(T,255,224))
Extract(and(S,T),31,0) -> and(Extract(S,31,0),Extract(T,31,0))
Extract(and(S,T),63,32) -> and(Extract(S,63,32),Extract(T,63,32))
Extract(and(S,T),95,64) -> and(Extract(S,95,64),Extract(T,95,64))
Extract(and(S,T),127,96) -> and(Extract(S,127,96),Extract(T,127,96))
Extract(and(S,T),159,128) -> and(Extract(S,159,128),Extract(T,159,128))
Extract(and(S,T),191,160) -> and(Extract(S,191,160),Extract(T,191,160))
Extract(and(S,T),223,192) -> and(Extract(S,223,192),Extract(T,223,192))
Extract(and(S,T),255,224) -> and(Extract(S,255,224),Extract(T,255,224))
Extract(or(S,T),63,0) -> or(Extract(S,63,0),Extract(T,63,0))
Extract(or(S,T),127,64) -> or(Extract(S,127,64),Extract(T,127,64))
Extract(or(S,T),191,128) -> or(Extract(S,191,128),Extract(T,191,128))
Extract(or(S,T),255,192) -> or(Extract(S,255,192),Extract(T,255,192))
Extract(and(S,T),63,0) -> and(Extract(S,63,0),Extract(T,63,0))
Extract(and(S,T),127,64) -> and(Extract(S,127,64),Extract(T,127,64))
Extract(and(S,T),191,128) -> and(Extract(S,191,128),Extract(T,191,128))
Extract(and(S,T),255,192) -> and(Extract(S,255,192),Extract(T,255,192))
Extract(xor(S,T),63,0) -> xor(Extract(S,63,0),Extract(T,63,0))
Extract(xor(S,T),127,64) -> xor(Extract(S,127,64),Extract(T,127,64))
Extract(xor(S,T),191,128) -> xor(Extract(S,191,128),Extract(T,191,128))
Extract(xor(S,T),255,192) -> xor(Extract(S,255,192),Extract(T,255,192))
Extract(or(S,T),127,0) -> or(Extract(S,127,0),Extract(T,127,0))
Extract(or(S,T),255,128) -> or(Extract(S,255,128),Extract(T,255,128))
Extract(and(S,T),127,0) -> and(Extract(S,127,0),Extract(T,127,0))
Extract(and(S,T),255,128) -> and(Extract(S,255,128),Extract(T,255,128))
xor(ZeroExt(C,31),Bits(32,0star1)) -> ZeroExt(invert(C),31)
invert(unsignedle(S,T)) -> unsignedlt(T,S)
sub(sub(Extract(Bits(64,B),63,32),Extract(Bits(64,A),63,32)),ZeroExt(unsignedlt(Extract(B,31,0),Extract(A,31,0)),31)) -> Extract(sub(B,A),63,32)
and(signedrshift(xor(BMINUSATOP=Extract(sub(Bits(64,B),Bits(64,A)),63,32),and(xor(BTOP=Extract(B,63,32),BMINUSATOP),BXORATOP=xor(ATOP=Extract(A,63,32),BTOP))),Bits(32,const31)),BXORATOP) -> xor(ATOP,Extract(signedmin(A,B),63,32))
and(signedrshift(xor(BMINUSATOP=Extract(sub(Bits(64,B),Bits(64,A)),63,32),and(xor(BTOP=Extract(B,63,32),BMINUSATOP),xor(Extract(A,63,32),BTOP))),Bits(32,const31)),xor(ABOT=Extract(A,31,0),Extract(B,31,0))) -> xor(ABOT,Extract(signedmin(A,B),31,0))
xor(Extract(B,31,0),xor(Extract(A,31,0),Extract(signedmin(A,B),31,0))) -> Extract(signedmax(A,B),31,0)
xor(Extract(B,63,32),xor(Extract(A,63,32),Extract(signedmin(A,B),63,32))) -> Extract(signedmax(A,B),63,32)
xor(xor(Extract(Bits(64,S),63,32),xor(Extract(signedmax(T,S),63,32),Extract(X,63,32))),Extract(T,63,32)) -> xor(Extract(X,63,32),Extract(signedmin(T,S),63,32))
xor(and(signedrshift(xor(BMINUSA=sub(B,A),and(xor(B,BMINUSA),AXORB=xor(A,B))),Bits(32,const31)),AXORB),A) -> signedmin(A,B)
xor(and(signedrshift(xor(BMINUSA=sub(B,A),and(xor(B,BMINUSA),AXORB=xor(A,B))),Bits(32,const31)),AXORB),B) -> signedmax(A,B)
and(signedrshift(xor(BMINUSATOP=Extract(sub(Bits(64,signedmax(A,B)),Bits(64,signedmin(A,B))),63,32),and(xor(BTOP=Extract(signedmax(A,B),63,32),BMINUSATOP),BAORATOP=xor(ATOP=Extract(signedmin(A,B),63,32),BTOP))),Bits(32,const31)),BAORATOP) -> xor(ATOP,Extract(signedmin(A,B),63,32))
and(signedrshift(xor(BMINUSATOP=Extract(sub(Bits(64,signedmax(A,B)),Bits(64,signedmin(A,B))),63,32),and(xor(BTOP=Extract(signedmax(A,B),63,32),BMINUSATOP),xor(Extract(signedmin(A,B),63,32),BTOP))),Bits(32,const31)),xor(ABOT=Extract(signedmin(A,B),31,0),Extract(signedmax(A,B),31,0))) -> xor(ABOT,Extract(signedmin(A,B),31,0))
signedrshift(xor(MINUSTOP=Extract(sub(MAX=signedmax(Bits(64,A),Bits(64,B)),signedmin(A,B)),63,32),and(xor(Extract(MAX,63,32),MINUSTOP),xor(Extract(A,63,32),Extract(B,63,32)))),Bits(32,const31)) -> 0star