set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
defpred S1[ Nat] means for x, y being nonpair-yielding FinSeqLen of holds InputVertices ($1 -BitGFA0Str x,y) = (rng x) \/ (rng y);
A1:
S1[ 0 ]
A3:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
:: thesis: ( S1[i] implies S1[i + 1] )
assume A4:
S1[
i]
;
:: thesis: S1[i + 1]
X:
i in NAT
by ORDINAL1:def 13;
let x,
y be
nonpair-yielding FinSeqLen of ;
:: thesis: InputVertices ((i + 1) -BitGFA0Str x,y) = (rng x) \/ (rng y)
consider x' being
nonpair-yielding FinSeqLen of ,
z1 being non
pair set such that A5:
x = x' ^ <*z1*>
by X, FACIRC_2:36;
consider y' being
nonpair-yielding FinSeqLen of ,
z2 being non
pair set such that A6:
y = y' ^ <*z2*>
by X, FACIRC_2:36;
A7:
1
in Seg 1
by FINSEQ_1:3;
then A8:
1
in dom <*z1*>
by FINSEQ_1:def 8;
len x' = i
by FINSEQ_1:def 18;
then A9:
x . (i + 1) =
<*z1*> . 1
by A5, A8, FINSEQ_1:def 7
.=
z1
by FINSEQ_1:def 8
;
A10:
1
in dom <*z2*>
by A7, FINSEQ_1:def 8;
len y' = i
by FINSEQ_1:def 18;
then A11:
y . (i + 1) =
<*z2*> . 1
by A6, A10, FINSEQ_1:def 7
.=
z2
by FINSEQ_1:def 8
;
deffunc H1(
Nat)
-> Element of
InnerVertices ($1 -BitGFA0Str x,y) = $1
-BitGFA0CarryOutput x,
y;
A12:
{z1,z2,H1(i)} = {H1(i),z1,z2}
by ENUMSET1:100;
A13:
rng x =
(rng x') \/ (rng <*z1*>)
by A5, FINSEQ_1:44
.=
(rng x') \/ {z1}
by FINSEQ_1:55
;
A14:
rng y =
(rng y') \/ (rng <*z2*>)
by A6, FINSEQ_1:44
.=
(rng y') \/ {z2}
by FINSEQ_1:55
;
A15:
(
z1 <> [<*z2,H1(i)*>,and2 ] &
z2 <> [<*H1(i),z1*>,and2 ] &
H1(
i)
<> [<*z1,z2*>,and2 ] &
H1(
i)
<> [<*z1,z2*>,xor2 ] )
by Lm2;
(
x' = x' ^ {} &
y' = y' ^ {} )
by FINSEQ_1:47;
then
i -BitGFA0Str x,
y = i -BitGFA0Str x',
y'
by A5, A6, Th5;
hence InputVertices ((i + 1) -BitGFA0Str x,y) =
(InputVertices (i -BitGFA0Str x',y')) \/ ((InputVertices (BitGFA0Str z1,z2,H1(i))) \ {H1(i)})
by A9, A11, Th12
.=
((rng x') \/ (rng y')) \/ ((InputVertices (BitGFA0Str z1,z2,H1(i))) \ {H1(i)})
by A4
.=
((rng x') \/ (rng y')) \/ ({z1,z2,H1(i)} \ {H1(i)})
by A15, GFACIRC1:41
.=
((rng x') \/ (rng y')) \/ {z1,z2}
by A12, ENUMSET1:136
.=
((rng x') \/ (rng y')) \/ ({z1} \/ {z2})
by ENUMSET1:41
.=
(((rng x') \/ (rng y')) \/ {z1}) \/ {z2}
by XBOOLE_1:4
.=
(((rng x') \/ {z1}) \/ (rng y')) \/ {z2}
by XBOOLE_1:4
.=
(rng x) \/ (rng y)
by A13, A14, XBOOLE_1:4
;
:: thesis: verum
end;
thus
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A3); :: thesis: verum