set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f4 = or3 ;
set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
deffunc H₁( Nat) -> Element of InnerVertices (n -BitGFA0Str (x,y)) = n -BitGFA0CarryOutput (x,y);
A1: ex h being ManySortedSet of NAT st
( H₁( 0 ) = h . 0 & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) by Def3;
defpred S₁[ Nat] means n -BitGFA0CarryOutput (x,y) is pair ;
A2: S₁[ 0 ] by A1;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set c = n -BitGFA0CarryOutput (x,y);
H₁(n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))) by Th7
.= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2],[<*(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))*>,and2],[<*(n -BitGFA0CarryOutput (x,y)),(x . (n + 1))*>,and2]*>,or3] ;
hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence n -BitGFA0CarryOutput (x,y) is pair ; :: thesis: verum