let x, b be non pair set ; :: thesis: ( x in the carrier of (BitCompStr (x,b)) & b in the carrier of (BitCompStr (x,b)) & [<*x,b*>,xor2a] in the carrier of (BitCompStr (x,b)) & [<*x,b*>,and2a] in the carrier of (BitCompStr (x,b)) )
set p = <*x,b*>;
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
A1: ( [<*x,b*>,xor2a] in the carrier of (CompStr (x,b)) & [<*x,b*>,and2a] in the carrier of (IncrementStr (x,b)) ) by FACIRC_1:43;
( x in the carrier of (CompStr (x,b)) & b in the carrier of (CompStr (x,b)) ) by FACIRC_1:43;
hence ( x in the carrier of (BitCompStr (x,b)) & b in the carrier of (BitCompStr (x,b)) & [<*x,b*>,xor2a] in the carrier of (BitCompStr (x,b)) & [<*x,b*>,and2a] in the carrier of (BitCompStr (x,b)) ) by A1, FACIRC_1:20; :: thesis: verum