let n be Nat; for ap, bm, cp, dm being FinSequence holds n -BitFTA1Circ (ap,bm,cp,dm) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (n -BitFTA1Layer2Circ (ap,bm,cp,dm))
let ap, bm, cp, dm be FinSequence; n -BitFTA1Circ (ap,bm,cp,dm) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (n -BitFTA1Layer2Circ (ap,bm,cp,dm))
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
defpred S1[ Nat] means $1 -BitFTA1Circ (ap,bm,cp,dm) = ($1 -BitFTA1Layer1Circ (ap,bm,cp)) +* ($1 -BitFTA1Layer2Circ (ap,bm,cp,dm));
A1:
S1[ 0 ]
proof
B1:
0 -BitFTA1Layer1Circ (
ap,
bm,
cp)
= 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
proof
consider f,
g being
ManySortedSet of
NAT such that
0 -BitFTA1Layer1Str (
ap,
bm,
cp)
= f . 0
and C1:
0 -BitFTA1Layer1Circ (
ap,
bm,
cp)
= g . 0
and
f . 0 = 1GateCircStr (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
and C2:
g . 0 = 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
and
for
k being
Nat for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra over
S st
S = f . k &
A = g . k holds
(
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) &
g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) )
by Def12;
thus
0 -BitFTA1Layer1Circ (
ap,
bm,
cp)
= 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
by C1, C2;
verum
end;
B2:
0 -BitFTA1Layer2Circ (
ap,
bm,
cp,
dm)
= 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
proof
consider f,
g,
h being
ManySortedSet of
NAT such that
0 -BitFTA1Layer2Str (
ap,
bm,
cp,
dm)
= f . 0
and C1:
0 -BitFTA1Layer2Circ (
ap,
bm,
cp,
dm)
= g . 0
and
f . 0 = 1GateCircStr (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
and C2:
g . 0 = 1GateCircuit (
<*>,
((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
A being
non-empty MSAlgebra over
S for
z being
set st
S = f . k &
A = g . k &
z = h . k holds
(
f . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) &
g . (k + 1) = A +* (BitGFA2Circ ((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 Def14;
thus
0 -BitFTA1Layer2Circ (
ap,
bm,
cp,
dm)
= 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
by C1, C2;
verum
end;
set sa = the
Sorts of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)));
set ca = the
Charact of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)));
B3:
the
Sorts of
((0 -BitFTA1Layer1Circ (ap,bm,cp)) +* (0 -BitFTA1Layer2Circ (ap,bm,cp,dm))) = the
Sorts of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)))
proof
the
Sorts of
((0 -BitFTA1Layer1Circ (ap,bm,cp)) +* (0 -BitFTA1Layer2Circ (ap,bm,cp,dm))) =
the
Sorts of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* the
Sorts of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)))
by B1, B2, CIRCCOMB:def 4
.=
the
Sorts of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)))
;
hence
the
Sorts of
((0 -BitFTA1Layer1Circ (ap,bm,cp)) +* (0 -BitFTA1Layer2Circ (ap,bm,cp,dm))) = the
Sorts of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)))
;
verum
the
Charact of
((0 -BitFTA1Layer1Circ (ap,bm,cp)) +* (0 -BitFTA1Layer2Circ (ap,bm,cp,dm))) =
the
Charact of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* the
Charact of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)))
by B1, B2, CIRCCOMB:def 4
.=
the
Charact of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)))
;
hence
S1[
0 ]
by Th13, B3;
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]
set Lk1 =
k -BitFTA1Layer1Circ (
ap,
bm,
cp);
set Lk2 =
k -BitFTA1Layer2Circ (
ap,
bm,
cp,
dm);
set cc =
k -BitFTA1CarryOutput (
ap,
bm,
cp,
dm);
set s1 =
BitGFA1Circ (
(ap . (k + 1)),
(bm . (k + 1)),
(cp . (k + 1)));
set s2 =
BitGFA2Circ (
(GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),
(k -BitFTA1CarryOutput (ap,bm,cp,dm)),
(dm . (k + 1)));
set cell =
BitFTA1Circ (
(ap . (k + 1)),
(bm . (k + 1)),
(cp . (k + 1)),
(dm . (k + 1)),
(k -BitFTA1CarryOutput (ap,bm,cp,dm)));
B2:
(k + 1) -BitFTA1Circ (
ap,
bm,
cp,
dm)
= (k -BitFTA1Circ (ap,bm,cp,dm)) +* (BitFTA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)),(dm . (k + 1)),(k -BitFTA1CarryOutput (ap,bm,cp,dm))))
by Th14;
B3:
(k + 1) -BitFTA1Layer1Circ (
ap,
bm,
cp)
= (k -BitFTA1Layer1Circ (ap,bm,cp)) +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))
by LmT16A;
B4:
(k + 1) -BitFTA1Layer2Circ (
ap,
bm,
cp,
dm)
= (k -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))
by LmT16B;
set l1 = the
Sorts of
(k -BitFTA1Layer1Circ (ap,bm,cp));
set l2 = the
Sorts of
(k -BitFTA1Layer2Circ (ap,bm,cp,dm));
set t1 = the
Sorts of
(BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))));
set t2 = the
Sorts of
(BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))));
set d1 = the
Charact of
(k -BitFTA1Layer1Circ (ap,bm,cp));
set d2 = the
Charact of
(k -BitFTA1Layer2Circ (ap,bm,cp,dm));
set e1 = the
Charact of
(BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))));
set e2 = the
Charact of
(BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))));
B5:
the
Sorts of
(k -BitFTA1Layer1Circ (ap,bm,cp)) tolerates the
Sorts of
(k -BitFTA1Layer2Circ (ap,bm,cp,dm))
by CIRCCOMB:59;
B6:
the
Sorts of
(BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) tolerates the
Sorts of
(BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))
by CIRCCOMB:59;
B7:
the
Sorts of
(k -BitFTA1Layer1Circ (ap,bm,cp)) tolerates the
Sorts of
(BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))
by CIRCCOMB:59;
B8:
the
Sorts of
(k -BitFTA1Layer2Circ (ap,bm,cp,dm)) tolerates the
Sorts of
(BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))
by CIRCCOMB:59;
B9:
the
Sorts of
(k -BitFTA1Circ (ap,bm,cp,dm)) tolerates the
Sorts of
(BitFTA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)),(dm . (k + 1)),(k -BitFTA1CarryOutput (ap,bm,cp,dm))))
by CIRCCOMB:59;
B10:
the
Sorts of
((k + 1) -BitFTA1Layer1Circ (ap,bm,cp)) tolerates the
Sorts of
((k + 1) -BitFTA1Layer2Circ (ap,bm,cp,dm))
by CIRCCOMB:59;
B11: the
Sorts of
((k + 1) -BitFTA1Circ (ap,bm,cp,dm)) =
the
Sorts of
((k -BitFTA1Layer1Circ (ap,bm,cp)) +* (k -BitFTA1Layer2Circ (ap,bm,cp,dm))) +* the
Sorts of
((BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B1, B9, CIRCCOMB:def 4, B2
.=
( the Sorts of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Sorts of (k -BitFTA1Layer2Circ (ap,bm,cp,dm))) +* the
Sorts of
((BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B5, CIRCCOMB:def 4
.=
( the Sorts of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Sorts of (k -BitFTA1Layer2Circ (ap,bm,cp,dm))) +* ( the Sorts of (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* the Sorts of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B6, CIRCCOMB:def 4
;
B12: the
Sorts of
(((k + 1) -BitFTA1Layer1Circ (ap,bm,cp)) +* ((k + 1) -BitFTA1Layer2Circ (ap,bm,cp,dm))) =
the
Sorts of
((k -BitFTA1Layer1Circ (ap,bm,cp)) +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* the
Sorts of
((k -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B4, B3, B10, CIRCCOMB:def 4
.=
( the Sorts of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Sorts of (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* the
Sorts of
((k -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B7, CIRCCOMB:def 4
.=
( the Sorts of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Sorts of (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* ( the Sorts of (k -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* the Sorts of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B8, CIRCCOMB:def 4
;
B13:
the
Sorts of
((k + 1) -BitFTA1Circ (ap,bm,cp,dm)) = the
Sorts of
(((k + 1) -BitFTA1Layer1Circ (ap,bm,cp)) +* ((k + 1) -BitFTA1Layer2Circ (ap,bm,cp,dm)))
by CIRCCOMB:59, LmF, B11, B12;
B14: the
Charact of
((k + 1) -BitFTA1Circ (ap,bm,cp,dm)) =
the
Charact of
((k -BitFTA1Layer1Circ (ap,bm,cp)) +* (k -BitFTA1Layer2Circ (ap,bm,cp,dm))) +* the
Charact of
((BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B1, B9, CIRCCOMB:def 4, B2
.=
( the Charact of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Charact of (k -BitFTA1Layer2Circ (ap,bm,cp,dm))) +* the
Charact of
((BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B5, CIRCCOMB:def 4
.=
( the Charact of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Charact of (k -BitFTA1Layer2Circ (ap,bm,cp,dm))) +* ( the Charact of (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* the Charact of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B6, CIRCCOMB:def 4
;
B15: the
Charact of
(((k + 1) -BitFTA1Layer1Circ (ap,bm,cp)) +* ((k + 1) -BitFTA1Layer2Circ (ap,bm,cp,dm))) =
the
Charact of
((k -BitFTA1Layer1Circ (ap,bm,cp)) +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* the
Charact of
((k -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B4, B3, B10, CIRCCOMB:def 4
.=
( the Charact of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Charact of (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* the
Charact of
((k -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B7, CIRCCOMB:def 4
.=
( the Charact of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Charact of (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* ( the Charact of (k -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* the Charact of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by B8, CIRCCOMB:def 4
;
( the Charact of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Charact of (k -BitFTA1Layer2Circ (ap,bm,cp,dm))) +* ( the Charact of (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) +* the Charact of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1))))) = ( the Charact of (k -BitFTA1Layer1Circ (ap,bm,cp)) +* the Charact of (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))) +* ( the Charact of (k -BitFTA1Layer2Circ (ap,bm,cp,dm)) +* the Charact of (BitGFA2Circ ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(k -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (k + 1)))))
by CIRCCOMB:48, LmF;
hence
S1[
k + 1]
by B13, B14, B15;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
hence
n -BitFTA1Circ (ap,bm,cp,dm) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (n -BitFTA1Layer2Circ (ap,bm,cp,dm))
; verum