theorem Th14:
for
ap,
bm,
cp,
dm,
cin being
set holds
(
ap in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
bm in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
cp in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
dm in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
cin in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
[<*ap,bm*>,xor2c] in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
GFA1AdderOutput (
ap,
bm,
cp)
in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
[<*ap,bm*>,and2c] in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
[<*bm,cp*>,and2a] in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
[<*cp,ap*>,and2] in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
GFA1CarryOutput (
ap,
bm,
cp)
in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
GFA2AdderOutput (
(GFA1AdderOutput (ap,bm,cp)),
cin,
dm)
in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
[<*cin,dm*>,and2c] in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) &
GFA2CarryOutput (
(GFA1AdderOutput (ap,bm,cp)),
cin,
dm)
in the
carrier of
(BitFTA1Str (ap,bm,cp,dm,cin)) )