let o1, o2 be Element of InnerVertices (n -BitAdderStr (x,y)); :: thesis: ( 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) ; :: thesis: ( 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) ; :: thesis: o1 = o2
deffunc H₁( 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) = H₁(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) = H₁(n,h2 . n) by A6;
h1 = h2 from NAT_1:sch 15(A7, A8, A9, A10, A11, A12);
hence o1 = o2 by A1, A4; :: thesis: verum