set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f4 = or3 ;
set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
deffunc H1( Nat) -> Element of InnerVertices (n -BitGFA0Str (x,y)) = n -BitGFA0CarryOutput (x,y);
A1:
ex h being ManySortedSet of NAT st
( H1( 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 S1[ Nat] means n -BitGFA0CarryOutput (x,y) is pair ;
A2:
S1[ 0 ]
by A1;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
set c =
n -BitGFA0CarryOutput (
x,
y);
H1(
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
(
S1[
n] implies
S1[
n + 1] )
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
hence
n -BitGFA0CarryOutput (x,y) is pair
; verum