defpred S1[ set , set , set ] means verum;
deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitAdderWithOverflowStr (x . ($3 + 1)),(y . ($3 + 1)),$2);
deffunc H2( set , Nat) -> Element of InnerVertices (MajorityStr (x . ($2 + 1)),(y . ($2 + 1)),$1) = MajorityOutput (x . ($2 + 1)),(y . ($2 + 1)),$1;
consider f, g being ManySortedSet of such that
A5:
( n -BitAdderStr x,y = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] )
and
A6:
for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = H1(S,z,n) & g . (n + 1) = H2(z,n) )
by Def3;
defpred S2[ Element of NAT ] means ex S being non empty ManySortedSign st
( S = f . $1 & g . $1 in InnerVertices S );
InnerVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) = {[<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )]}
by CIRCCOMB:49;
then
[<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] in InnerVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ))
by TARSKI:def 1;
then A7:
S2[ 0 ]
by A5;
A8:
for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be
Element of
NAT ;
:: thesis: ( S2[i] implies S2[i + 1] )
assume that A9:
ex
S being non
empty ManySortedSign st
(
S = f . i &
g . i in InnerVertices S )
and A10:
for
S being non
empty ManySortedSign st
S = f . (i + 1) holds
not
g . (i + 1) in InnerVertices S
;
:: thesis: contradiction
consider S being non
empty ManySortedSign such that A11:
(
S = f . i &
g . i in InnerVertices S )
by A9;
MajorityOutput (x . (i + 1)),
(y . (i + 1)),
(g . i) in InnerVertices (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(g . i))
by FACIRC_1:90;
then
(
MajorityOutput (x . (i + 1)),
(y . (i + 1)),
(g . i) in InnerVertices (S +* (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(g . i))) &
f . (i + 1) = S +* (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(g . i)) &
g . (i + 1) = MajorityOutput (x . (i + 1)),
(y . (i + 1)),
(g . i) )
by A6, A11, FACIRC_1:22;
hence
contradiction
by A10;
:: thesis: verum
end;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
for i being Element of NAT holds S2[i]
from NAT_1:sch 1(A7, A8);
then
ex S being non empty ManySortedSign st
( S = f . n' & g . n in InnerVertices S )
;
then reconsider o = g . n' as Element of InnerVertices (n -BitAdderStr x,y) by A5;
take
o
; :: thesis: ex h being ManySortedSet of st
( o = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput (x . (n + 1)),(y . (n + 1)),z ) )
take
g
; :: thesis: ( o = g . n & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for z being set st z = g . n holds
g . (n + 1) = MajorityOutput (x . (n + 1)),(y . (n + 1)),z ) )
thus
( o = g . n & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] )
by A5; :: thesis: for n being Nat
for z being set st z = g . n holds
g . (n + 1) = MajorityOutput (x . (n + 1)),(y . (n + 1)),z
let i be Nat; :: thesis: for z being set st z = g . i holds
g . (i + 1) = MajorityOutput (x . (i + 1)),(y . (i + 1)),z
A12:
ex S being non empty ManySortedSign ex x being set st
( S = f . 0 & x = g . 0 & S1[S,x, 0 ] )
by A5;
A13:
for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = g . n & S1[S,x,n] holds
S1[H1(S,x,n),H2(x,n),n + 1]
;
for n being Nat ex S being non empty ManySortedSign st
( S = f . n & S1[S,g . n,n] )
from CIRCCMB2:sch 2(A12, A6, A13);
then
ex S being non empty ManySortedSign st S = f . i
;
hence
for z being set st z = g . i holds
g . (i + 1) = MajorityOutput (x . (i + 1)),(y . (i + 1)),z
by A6; :: thesis: verum