defpred S1[ Nat] means for x, y being nonpair-yielding FinSeqLen of $1 holds InputVertices ($1 -BitAdderStr (x,y)) = (rng x) \/ (rng y);
A1:
S1[ 0 ]
A2:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A3:
S1[
i]
;
S1[i + 1]
let x,
y be
nonpair-yielding FinSeqLen of
i + 1;
InputVertices ((i + 1) -BitAdderStr (x,y)) = (rng x) \/ (rng y)
consider x9 being
nonpair-yielding FinSeqLen of
i,
z1 being non
pair set such that A4:
x = x9 ^ <*z1*>
by Lm2;
consider y9 being
nonpair-yielding FinSeqLen of
i,
z2 being non
pair set such that A5:
y = y9 ^ <*z2*>
by Lm2;
set S =
(i + 1) -BitAdderStr (
x,
y);
A6:
1
in Seg 1
by FINSEQ_1:1;
A7:
dom <*z1*> = Seg 1
by FINSEQ_1:def 8;
A8:
<*z1*> . 1
= z1
;
len x9 = i
by CARD_1:def 7;
then A9:
x . (i + 1) = z1
by A4, A6, A7, A8, FINSEQ_1:def 7;
A10:
dom <*z2*> = Seg 1
by FINSEQ_1:def 8;
A11:
<*z2*> . 1
= z2
;
len y9 = i
by CARD_1:def 7;
then A12:
y . (i + 1) = z2
by A5, A6, A10, A11, FINSEQ_1:def 7;
A13:
{z1,z2,(i -BitMajorityOutput (x,y))} = {(i -BitMajorityOutput (x,y)),z1,z2}
by ENUMSET1:59;
A14:
rng x =
(rng x9) \/ (rng <*z1*>)
by A4, FINSEQ_1:31
.=
(rng x9) \/ {z1}
by FINSEQ_1:38
;
A15:
rng y =
(rng y9) \/ (rng <*z2*>)
by A5, FINSEQ_1:31
.=
(rng y9) \/ {z2}
by FINSEQ_1:38
;
A16:
i -BitMajorityOutput (
x,
y)
<> [<*z1,z2*>,'&']
by Th25;
A17:
i -BitMajorityOutput (
x,
y)
<> [<*z1,z2*>,'xor']
by Th25;
A18:
x9 = x9 ^ {}
by FINSEQ_1:34;
y9 = y9 ^ {}
by FINSEQ_1:34;
then
i -BitAdderStr (
x,
y)
= i -BitAdderStr (
x9,
y9)
by A4, A5, A18, Th10;
hence InputVertices ((i + 1) -BitAdderStr (x,y)) =
(InputVertices (i -BitAdderStr (x9,y9))) \/ ((InputVertices (BitAdderWithOverflowStr (z1,z2,(i -BitMajorityOutput (x,y))))) \ {(i -BitMajorityOutput (x,y))})
by A9, A12, Th26
.=
((rng x9) \/ (rng y9)) \/ ((InputVertices (BitAdderWithOverflowStr (z1,z2,(i -BitMajorityOutput (x,y))))) \ {(i -BitMajorityOutput (x,y))})
by A3
.=
((rng x9) \/ (rng y9)) \/ ({z1,z2,(i -BitMajorityOutput (x,y))} \ {(i -BitMajorityOutput (x,y))})
by A16, A17, Th22
.=
((rng x9) \/ (rng y9)) \/ {z1,z2}
by A13, ENUMSET1:86
.=
((rng x9) \/ (rng y9)) \/ ({z1} \/ {z2})
by ENUMSET1:1
.=
(((rng x9) \/ (rng y9)) \/ {z1}) \/ {z2}
by XBOOLE_1:4
.=
(((rng x9) \/ {z1}) \/ (rng y9)) \/ {z2}
by XBOOLE_1:4
.=
(rng x) \/ (rng y)
by A14, A15, XBOOLE_1:4
;
verum
end;
thus
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A2); verum