set o0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )];
deffunc H₁( Nat, set ) -> Element of InnerVertices (GFA1CarryStr (x . ($1 + 1)),(y . ($1 + 1)),$2) = GFA1CarryOutput (x . ($1 + 1)),(y . ($1 + 1)),$2;
let o1, o2 be Element of InnerVertices (n -BitGFA1Str x,y); :: thesis: ( ex h being ManySortedSet of NAT st
( o1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) & ex h being ManySortedSet of NAT st
( o2 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) implies o1 = o2 )
given h1 being ManySortedSet of NAT such that A1: ( o1 = h1 . n & h1 . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h1 . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h1 . n) ) ) ; :: thesis: ( for h being ManySortedSet of NAT holds
( not o2 = h . n or not h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] or ex n being Nat st not h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) or o1 = o2 )
given h2 being ManySortedSet of NAT such that A2: ( o2 = h2 . n & h2 . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h2 . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h2 . n) ) ) ; :: thesis: o1 = o2
A3: dom h1 = NAT by PBOOLE:def 3;
B3: h1 . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] by A1;
C3: for n being Nat holds h1 . (n + 1) = H₁(n,h1 . n) by A1;
A4: dom h2 = NAT by PBOOLE:def 3;
B4: h2 . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] by A2;
C4: for n being Nat holds h2 . (n + 1) = H₁(n,h2 . n) by A2;
h1 = h2 from NAT_1:sch 15(A3, B3, C3, A4, B4, C4);
hence o1 = o2 by A1, A2; :: thesis: verum