defpred S1[ Nat] means for ap, bm, cp, dm being FinSequence holds $1 -BitFTA1Str (ap,bm,cp,dm) = ($1 -BitFTA1Layer1Str (ap,bm,cp)) +* ($1 -BitFTA1Layer2Str (ap,bm,cp,dm));
A1:
S1[ 0 ]
proof
let ap,
bm,
cp,
dm be
FinSequence;
0 -BitFTA1Str (ap,bm,cp,dm) = (0 -BitFTA1Layer1Str (ap,bm,cp)) +* (0 -BitFTA1Layer2Str (ap,bm,cp,dm))
set s0 =
1GateCircStr (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE));
consider f being
ManySortedSet of
NAT such that B1:
0 -BitFTA1Layer1Str (
ap,
bm,
cp)
= f . 0
and B2:
f . 0 = 1GateCircStr (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
and
for
k being
Nat for
S being non
empty ManySortedSign st
S = f . k holds
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))
by Def11;
consider g,
h being
ManySortedSet of
NAT such that B3:
0 -BitFTA1Layer2Str (
ap,
bm,
cp,
dm)
= g . 0
and B4:
g . 0 = 1GateCircStr (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
and
h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
for
k being
Nat for
S being non
empty ManySortedSign for
z being
set st
S = g . k &
z = h . k holds
(
g . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) &
h . (k + 1) = GFA1CarryOutput (
(ap . (k + 1)),
(bm . (k + 1)),
(cp . (k + 1))) )
by Def13;
(1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) = 1GateCircStr (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
by CIRCCOMB:4;
hence
0 -BitFTA1Str (
ap,
bm,
cp,
dm)
= (0 -BitFTA1Layer1Str (ap,bm,cp)) +* (0 -BitFTA1Layer2Str (ap,bm,cp,dm))
by B1, B2, B3, B4, Th13;
verum
end;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume B1:
S1[
k]
;
S1[k + 1]
let ap,
bm,
cp,
dm be
FinSequence;
(k + 1) -BitFTA1Str (ap,bm,cp,dm) = ((k + 1) -BitFTA1Layer1Str (ap,bm,cp)) +* ((k + 1) -BitFTA1Layer2Str (ap,bm,cp,dm))
set a =
k -BitFTA1Layer1Str (
ap,
bm,
cp);
set b =
k -BitFTA1Layer2Str (
ap,
bm,
cp,
dm);
set s1 =
BitGFA1Str (
(ap . (k + 1)),
(bm . (k + 1)),
(cp . (k + 1)));
set s2 =
BitGFA2Str (
(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),
(k -BitFTA1CarryOutput (ap,bm,cp,dm)),
(dm . (k + 1)));
B2:
k -BitFTA1Str (
ap,
bm,
cp,
dm)
= (k -BitFTA1Layer1Str (ap,bm,cp)) +* (k -BitFTA1Layer2Str (ap,bm,cp,dm))
by B1;
B3:
BitFTA1Str (
(ap . (k + 1)),
(bm . (k + 1)),
(cp . (k + 1)),
(dm . (k + 1)),
(k -BitFTA1CarryOutput (ap,bm,cp,dm)))
= (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))
;
B4:
(k + 1) -BitFTA1Str (
ap,
bm,
cp,
dm)
= ((k -BitFTA1Layer1Str (ap,bm,cp)) +* (k -BitFTA1Layer2Str (ap,bm,cp,dm))) +* ((BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by Th14, B2, B3;
B5:
(k + 1) -BitFTA1Layer2Str (
ap,
bm,
cp,
dm)
= (k -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))
by LmT15B;
((k -BitFTA1Layer1Str (ap,bm,cp)) +* (k -BitFTA1Layer2Str (ap,bm,cp,dm))) +* ((BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))) =
(k -BitFTA1Layer1Str (ap,bm,cp)) +* ((k -BitFTA1Layer2Str (ap,bm,cp,dm)) +* ((BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))))
by CIRCCOMB:6
.=
(k -BitFTA1Layer1Str (ap,bm,cp)) +* (((k -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by CIRCCOMB:6
.=
(k -BitFTA1Layer1Str (ap,bm,cp)) +* (((BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (k -BitFTA1Layer2Str (ap,bm,cp,dm))) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by FACIRC_1:23
.=
(k -BitFTA1Layer1Str (ap,bm,cp)) +* ((BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* ((k -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))))
by CIRCCOMB:6
.=
((k -BitFTA1Layer1Str (ap,bm,cp)) +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* ((k -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by CIRCCOMB:6
;
hence
(k + 1) -BitFTA1Str (
ap,
bm,
cp,
dm)
= ((k + 1) -BitFTA1Layer1Str (ap,bm,cp)) +* ((k + 1) -BitFTA1Layer2Str (ap,bm,cp,dm))
by B4, LmT15A, B5;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
for n being Nat
for ap, bm, cp, dm being FinSequence holds n -BitFTA1Str (ap,bm,cp,dm) = (n -BitFTA1Layer1Str (ap,bm,cp)) +* (n -BitFTA1Layer2Str (ap,bm,cp,dm))
; verum