let n be Nat; for ap, bp, cp, dp being FinSequence holds n -BitFTA0Circ (ap,bp,cp,dp) = (n -BitFTA0Layer1Circ (ap,bp,cp)) +* (n -BitFTA0Layer2Circ (ap,bp,cp,dp))
let ap, bp, cp, dp be FinSequence; n -BitFTA0Circ (ap,bp,cp,dp) = (n -BitFTA0Layer1Circ (ap,bp,cp)) +* (n -BitFTA0Layer2Circ (ap,bp,cp,dp))
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
defpred S1[ Nat] means $1 -BitFTA0Circ (ap,bp,cp,dp) = ($1 -BitFTA0Layer1Circ (ap,bp,cp)) +* ($1 -BitFTA0Layer2Circ (ap,bp,cp,dp));
A1:
S1[ 0 ]
proof
B1:
0 -BitFTA0Layer1Circ (
ap,
bp,
cp)
= 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
proof
consider f,
g being
ManySortedSet of
NAT such that
0 -BitFTA0Layer1Str (
ap,
bp,
cp)
= f . 0
and C1:
0 -BitFTA0Layer1Circ (
ap,
bp,
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 +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) &
g . (k + 1) = A +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) )
by Def5;
thus
0 -BitFTA0Layer1Circ (
ap,
bp,
cp)
= 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
by C1, C2;
verum
end;
B2:
0 -BitFTA0Layer2Circ (
ap,
bp,
cp,
dp)
= 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE))
proof
consider f,
g,
h being
ManySortedSet of
NAT such that
0 -BitFTA0Layer2Str (
ap,
bp,
cp,
dp)
= f . 0
and C1:
0 -BitFTA0Layer2Circ (
ap,
bp,
cp,
dp)
= 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 +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) &
g . (k + 1) = A +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) &
h . (k + 1) = GFA0CarryOutput (
(ap . (k + 1)),
(bp . (k + 1)),
(cp . (k + 1))) )
by Def7;
thus
0 -BitFTA0Layer2Circ (
ap,
bp,
cp,
dp)
= 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 -BitFTA0Layer1Circ (ap,bp,cp)) +* (0 -BitFTA0Layer2Circ (ap,bp,cp,dp))) = the
Sorts of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)))
proof
the
Sorts of
((0 -BitFTA0Layer1Circ (ap,bp,cp)) +* (0 -BitFTA0Layer2Circ (ap,bp,cp,dp))) =
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 -BitFTA0Layer1Circ (ap,bp,cp)) +* (0 -BitFTA0Layer2Circ (ap,bp,cp,dp))) = the
Sorts of
(1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)))
;
verum
the
Charact of
((0 -BitFTA0Layer1Circ (ap,bp,cp)) +* (0 -BitFTA0Layer2Circ (ap,bp,cp,dp))) =
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 Th2, 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 -BitFTA0Layer1Circ (
ap,
bp,
cp);
set Lk2 =
k -BitFTA0Layer2Circ (
ap,
bp,
cp,
dp);
set cc =
k -BitFTA0CarryOutput (
ap,
bp,
cp,
dp);
set s1 =
BitGFA0Circ (
(ap . (k + 1)),
(bp . (k + 1)),
(cp . (k + 1)));
set s2 =
BitGFA0Circ (
(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),
(k -BitFTA0CarryOutput (ap,bp,cp,dp)),
(dp . (k + 1)));
set cell =
BitFTA0Circ (
(ap . (k + 1)),
(bp . (k + 1)),
(cp . (k + 1)),
(dp . (k + 1)),
(k -BitFTA0CarryOutput (ap,bp,cp,dp)));
B2:
(k + 1) -BitFTA0Circ (
ap,
bp,
cp,
dp)
= (k -BitFTA0Circ (ap,bp,cp,dp)) +* (BitFTA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)),(dp . (k + 1)),(k -BitFTA0CarryOutput (ap,bp,cp,dp))))
by Th3;
B3:
(k + 1) -BitFTA0Layer1Circ (
ap,
bp,
cp)
= (k -BitFTA0Layer1Circ (ap,bp,cp)) +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))
by LmT06A;
B4:
(k + 1) -BitFTA0Layer2Circ (
ap,
bp,
cp,
dp)
= (k -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))
by LmT06B;
set l1 = the
Sorts of
(k -BitFTA0Layer1Circ (ap,bp,cp));
set l2 = the
Sorts of
(k -BitFTA0Layer2Circ (ap,bp,cp,dp));
set t1 = the
Sorts of
(BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))));
set t2 = the
Sorts of
(BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))));
set d1 = the
Charact of
(k -BitFTA0Layer1Circ (ap,bp,cp));
set d2 = the
Charact of
(k -BitFTA0Layer2Circ (ap,bp,cp,dp));
set e1 = the
Charact of
(BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))));
set e2 = the
Charact of
(BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))));
B5:
the
Sorts of
(k -BitFTA0Layer1Circ (ap,bp,cp)) tolerates the
Sorts of
(k -BitFTA0Layer2Circ (ap,bp,cp,dp))
by CIRCCOMB:59;
B6:
the
Sorts of
(BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) tolerates the
Sorts of
(BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))
by CIRCCOMB:59;
B7:
the
Sorts of
(k -BitFTA0Layer1Circ (ap,bp,cp)) tolerates the
Sorts of
(BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))
by CIRCCOMB:59;
B8:
the
Sorts of
(k -BitFTA0Layer2Circ (ap,bp,cp,dp)) tolerates the
Sorts of
(BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))
by CIRCCOMB:59;
B9:
the
Sorts of
(k -BitFTA0Circ (ap,bp,cp,dp)) tolerates the
Sorts of
(BitFTA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)),(dp . (k + 1)),(k -BitFTA0CarryOutput (ap,bp,cp,dp))))
by CIRCCOMB:59;
B10:
the
Sorts of
((k + 1) -BitFTA0Layer1Circ (ap,bp,cp)) tolerates the
Sorts of
((k + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp))
by CIRCCOMB:59;
B11: the
Sorts of
((k + 1) -BitFTA0Circ (ap,bp,cp,dp)) =
the
Sorts of
((k -BitFTA0Layer1Circ (ap,bp,cp)) +* (k -BitFTA0Layer2Circ (ap,bp,cp,dp))) +* the
Sorts of
((BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B1, B9, CIRCCOMB:def 4, B2
.=
( the Sorts of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Sorts of (k -BitFTA0Layer2Circ (ap,bp,cp,dp))) +* the
Sorts of
((BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B5, CIRCCOMB:def 4
.=
( the Sorts of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Sorts of (k -BitFTA0Layer2Circ (ap,bp,cp,dp))) +* ( the Sorts of (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* the Sorts of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B6, CIRCCOMB:def 4
;
B12: the
Sorts of
(((k + 1) -BitFTA0Layer1Circ (ap,bp,cp)) +* ((k + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp))) =
the
Sorts of
((k -BitFTA0Layer1Circ (ap,bp,cp)) +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* the
Sorts of
((k -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B4, B3, B10, CIRCCOMB:def 4
.=
( the Sorts of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Sorts of (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* the
Sorts of
((k -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B7, CIRCCOMB:def 4
.=
( the Sorts of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Sorts of (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* ( the Sorts of (k -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* the Sorts of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B8, CIRCCOMB:def 4
;
B13:
the
Sorts of
((k + 1) -BitFTA0Circ (ap,bp,cp,dp)) = the
Sorts of
(((k + 1) -BitFTA0Layer1Circ (ap,bp,cp)) +* ((k + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp)))
by CIRCCOMB:59, LmF, B11, B12;
B14: the
Charact of
((k + 1) -BitFTA0Circ (ap,bp,cp,dp)) =
the
Charact of
((k -BitFTA0Layer1Circ (ap,bp,cp)) +* (k -BitFTA0Layer2Circ (ap,bp,cp,dp))) +* the
Charact of
((BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B1, B9, CIRCCOMB:def 4, B2
.=
( the Charact of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Charact of (k -BitFTA0Layer2Circ (ap,bp,cp,dp))) +* the
Charact of
((BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B5, CIRCCOMB:def 4
.=
( the Charact of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Charact of (k -BitFTA0Layer2Circ (ap,bp,cp,dp))) +* ( the Charact of (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* the Charact of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B6, CIRCCOMB:def 4
;
B15: the
Charact of
(((k + 1) -BitFTA0Layer1Circ (ap,bp,cp)) +* ((k + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp))) =
the
Charact of
((k -BitFTA0Layer1Circ (ap,bp,cp)) +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* the
Charact of
((k -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B4, B3, B10, CIRCCOMB:def 4
.=
( the Charact of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Charact of (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* the
Charact of
((k -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B7, CIRCCOMB:def 4
.=
( the Charact of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Charact of (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* ( the Charact of (k -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* the Charact of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))
by B8, CIRCCOMB:def 4
;
( the Charact of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Charact of (k -BitFTA0Layer2Circ (ap,bp,cp,dp))) +* ( the Charact of (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* the Charact of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))) = ( the Charact of (k -BitFTA0Layer1Circ (ap,bp,cp)) +* the Charact of (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* ( the Charact of (k -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* the Charact of (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (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 -BitFTA0Circ (ap,bp,cp,dp) = (n -BitFTA0Layer1Circ (ap,bp,cp)) +* (n -BitFTA0Layer2Circ (ap,bp,cp,dp))
; verum