let o1, o2 be Element of InnerVertices (n -BitAdderStr (x,y)); ( ex h being ManySortedSet of NAT st
( o1 = 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) ) ) & ex h being ManySortedSet of NAT st
( o2 = 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) ) ) implies o1 = o2 )
given h1 being ManySortedSet of NAT such that A1:
o1 = h1 . n
and
A2:
h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
A3:
for n being Nat
for z being set st z = h1 . n holds
h1 . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z)
; ( for h being ManySortedSet of NAT holds
( not o2 = h . n or not h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] or ex n being Nat ex z being set st
( z = h . n & not h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) or o1 = o2 )
given h2 being ManySortedSet of NAT such that A4:
o2 = h2 . n
and
A5:
h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
A6:
for n being Nat
for z being set st z = h2 . n holds
h2 . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z)
; o1 = o2
deffunc H1( Nat, set ) -> Element of InnerVertices (MajorityStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = MajorityOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
A7:
dom h1 = NAT
by PARTFUN1:def 2;
A8:
h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
by A2;
A9:
for n being Nat holds h1 . (n + 1) = H1(n,h1 . n)
by A3;
A10:
dom h2 = NAT
by PARTFUN1:def 2;
A11:
h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
by A5;
A12:
for n being Nat holds h2 . (n + 1) = H1(n,h2 . n)
by A6;
h1 = h2
from NAT_1:sch 15(A7, A8, A9, A10, A11, A12);
hence
o1 = o2
by A1, A4; verum