let S1, S2 be non empty ManySortedSign ; ( S1 is gate`2isBoolean & S2 is gate`2isBoolean implies S1 +* S2 is gate`2isBoolean )
set S = S1 +* S2;
assume that
A1:
S1 is gate`2isBoolean
and
A2:
S2 is gate`2isBoolean
; S1 +* S2 is gate`2isBoolean
let g be set ; CIRCCOMB:def 9 ( g in the carrier' of (S1 +* S2) implies for p being FinSequence st p = the Arity of (S1 +* S2) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
assume A3:
g in the carrier' of (S1 +* S2)
; for p being FinSequence st p = the Arity of (S1 +* S2) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
let p be FinSequence; ( p = the Arity of (S1 +* S2) . g implies ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
assume A4:
p = the Arity of (S1 +* S2) . g
; ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
reconsider g = g as Gate of (S1 +* S2) by A3;
A5:
dom the Arity of S1 = the carrier' of S1
by FUNCT_2:def 1;
A6:
the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2
by Def2;
A7:
dom the Arity of S2 = the carrier' of S2
by FUNCT_2:def 1;
A8:
the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2
by Def2;
then A9:
( g in the carrier' of S1 or g in the carrier' of S2 )
by A3, XBOOLE_0:def 3;
A10:
now ( not g in the carrier' of S2 implies ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )assume A11:
not
g in the
carrier' of
S2
;
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]then reconsider g1 =
g as
Gate of
S1 by A8, A3, XBOOLE_0:def 3;
the
Arity of
S1 . g1 = p
by A8, A6, A3, A4, A5, A7, A11, FUNCT_4:def 1;
hence
ex
f being
Function of
((len p) -tuples_on BOOLEAN),
BOOLEAN st
g = [(g `1),f]
by A1, A9, A11;
verum end;
now ( g in the carrier' of S2 implies ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )assume A12:
g in the
carrier' of
S2
;
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]then reconsider g2 =
g as
Gate of
S2 ;
the
Arity of
S2 . g2 = p
by A8, A6, A4, A5, A7, A12, FUNCT_4:def 1;
hence
ex
f being
Function of
((len p) -tuples_on BOOLEAN),
BOOLEAN st
g = [(g `1),f]
by A2, A12;
verum end;
hence
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
by A10; verum