set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f4 = or3 ;
set h0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )];
deffunc H₁( Nat) -> Element of InnerVertices (n -BitGFA1Str x,y) = n -BitGFA1CarryOutput x,y;
consider h being ManySortedSet of such that
A1: H₁( 0 ) = h . 0 and
A2: h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] and
for n being Nat holds h . (n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) by Def7;
defpred S₁[ Nat] means n -BitGFA1CarryOutput x,y is pair ;
A3: S₁[ 0 ] by A1, A2;
A4: 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 -BitGFA1CarryOutput x,y;
H₁(n + 1) = GFA1CarryOutput (x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput x,y) by Th21
.= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2c ],[<*(y . (n + 1)),(n -BitGFA1CarryOutput x,y)*>,and2a ],[<*(n -BitGFA1CarryOutput 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(A3, A4);
hence n -BitGFA1CarryOutput x,y is pair ; :: thesis: verum