defpred S1[ Element of NAT ] means for x, y being nonpair-yielding FinSeqLen of $1 holds InputVertices ($1 -BitSubtracterStr x,y) = (rng x) \/ (rng y);
A1:
S1[ 0 ]
A2:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be
Element of
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) -BitSubtracterStr 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 FACIRC_2:36;
consider y9 being
nonpair-yielding FinSeqLen of
i,
z2 being non
pair set such that A5:
y = y9 ^ <*z2*>
by FACIRC_2:36;
set S =
(i + 1) -BitSubtracterStr x,
y;
A6:
1
in Seg 1
by FINSEQ_1:3;
then A7:
1
in dom <*z1*>
by FINSEQ_1:def 8;
len x9 = i
by FINSEQ_1:def 18;
then A8:
x . (i + 1) =
<*z1*> . 1
by A4, A7, FINSEQ_1:def 7
.=
z1
by FINSEQ_1:def 8
;
A9:
1
in dom <*z2*>
by A6, FINSEQ_1:def 8;
len y9 = i
by FINSEQ_1:def 18;
then A10:
y . (i + 1) =
<*z2*> . 1
by A5, A9, FINSEQ_1:def 7
.=
z2
by FINSEQ_1:def 8
;
A11:
{z1,z2,(i -BitBorrowOutput x,y)} = {(i -BitBorrowOutput x,y),z1,z2}
by ENUMSET1:100;
A12:
rng x =
(rng x9) \/ (rng <*z1*>)
by A4, FINSEQ_1:44
.=
(rng x9) \/ {z1}
by FINSEQ_1:55
;
A13:
rng y =
(rng y9) \/ (rng <*z2*>)
by A5, FINSEQ_1:44
.=
(rng y9) \/ {z2}
by FINSEQ_1:55
;
A14:
i -BitBorrowOutput x,
y <> [<*z1,z2*>,and2a ]
by Th19;
A15:
i -BitBorrowOutput x,
y <> [<*z1,z2*>,'xor' ]
by Th19;
A16:
x9 = x9 ^ {}
by FINSEQ_1:47;
y9 = y9 ^ {}
by FINSEQ_1:47;
then
i -BitSubtracterStr x,
y = i -BitSubtracterStr x9,
y9
by A4, A5, A16, Th5;
hence InputVertices ((i + 1) -BitSubtracterStr x,y) =
(InputVertices (i -BitSubtracterStr x9,y9)) \/ ((InputVertices (BitSubtracterWithBorrowStr z1,z2,(i -BitBorrowOutput x,y))) \ {(i -BitBorrowOutput x,y)})
by A8, A10, Th20
.=
((rng x9) \/ (rng y9)) \/ ((InputVertices (BitSubtracterWithBorrowStr z1,z2,(i -BitBorrowOutput x,y))) \ {(i -BitBorrowOutput x,y)})
by A3
.=
((rng x9) \/ (rng y9)) \/ ({z1,z2,(i -BitBorrowOutput x,y)} \ {(i -BitBorrowOutput x,y)})
by A14, A15, Th16
.=
((rng x9) \/ (rng y9)) \/ {z1,z2}
by A11, ENUMSET1:136
.=
((rng x9) \/ (rng y9)) \/ ({z1} \/ {z2})
by ENUMSET1:41
.=
(((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 A12, A13, XBOOLE_1:4
;
verum
end;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A1, A2); verum