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;
( x in the carrier of (CompStr x,b) & b in the carrier of (CompStr x,b) & [<*x,b*>,xor2a ] in the carrier of (CompStr x,b) & x in the carrier of (IncrementStr x,b) & b in the carrier of (IncrementStr x,b) & [<*x,b*>,and2a ] in the carrier of (IncrementStr 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 FACIRC_1:20; :: thesis: verum