set o0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
deffunc H₁( Nat, set ) -> Element of InnerVertices (GFA0CarryStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = GFA0CarryOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
let o1, o2 be Element of InnerVertices (n -BitGFA0Str (x,y)); :: thesis: ( ex h being ManySortedSet of NAT st
( o1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) & ex h being ManySortedSet of NAT st
( o2 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) 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 holds h1 . (n + 1) = H₁(n,h1 . n) ; :: 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 st not h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) 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 holds h2 . (n + 1) = H₁(n,h2 . n) ; :: thesis: o1 = o2
A7: dom h1 = NAT by PARTFUN1:def 2;
A8: dom h2 = NAT by PARTFUN1:def 2;
h1 = h2 from NAT_1:sch 15(A7, A2, A3, A8, A5, A6);
hence o1 = o2 by A1, A4; :: thesis: verum