theorem Th4:
for
ap,
bp,
cp,
dp,
cin being
set holds
(
ap in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
bp in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
cp in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
dp in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
cin in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
[<*ap,bp*>,xor2] in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
GFA0AdderOutput (
ap,
bp,
cp)
in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
[<*ap,bp*>,and2] in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
[<*bp,cp*>,and2] in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
[<*cp,ap*>,and2] in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
GFA0CarryOutput (
ap,
bp,
cp)
in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
GFA0AdderOutput (
(GFA0AdderOutput (ap,bp,cp)),
cin,
dp)
in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
[<*cin,dp*>,and2] in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) &
GFA0CarryOutput (
(GFA0AdderOutput (ap,bp,cp)),
cin,
dp)
in the
carrier of
(BitFTA0Str (ap,bp,cp,dp,cin)) )