let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 is gate`2isBoolean & S2 is gate`2isBoolean implies S1 +* S2 is gate`2isBoolean )
set S = S1 +* S2;
assume A1:
( S1 is gate`2isBoolean & S2 is gate`2isBoolean )
; :: thesis: S1 +* S2 is gate`2isBoolean
A2:
( the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 & the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 )
by Def2;
let g be set ; :: according to CIRCCOMB:def 9 :: thesis: ( 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)
; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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:
( g in the carrier' of S1 or g in the carrier' of S2 )
by A2, A3, XBOOLE_0:def 3;
A6:
( dom the Arity of (S1 +* S2) = the carrier' of (S1 +* S2) & dom the Arity of S1 = the carrier' of S1 & dom the Arity of S2 = the carrier' of S2 )
by FUNCT_2:def 1;
A7:
now assume A8:
not
g in the
carrier' of
S2
;
:: thesis: 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 A2, A3, XBOOLE_0:def 3;
the
Arity of
S1 . g1 = p
by A2, A3, A4, A6, A8, FUNCT_4:def 1;
hence
ex
f being
Function of
((len p) -tuples_on BOOLEAN ),
BOOLEAN st
g = [(g `1 ),f]
by A1, A5, A8, Def9;
:: thesis: verum end;
now assume A9:
g in the
carrier' of
S2
;
:: thesis: 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 A2, A4, A6, A9, FUNCT_4:def 1;
hence
ex
f being
Function of
((len p) -tuples_on BOOLEAN ),
BOOLEAN st
g = [(g `1 ),f]
by A1, A9, Def9;
:: thesis: verum end;
hence
ex f being Function of ((len p) -tuples_on BOOLEAN ),BOOLEAN st g = [(g `1 ),f]
by A7; :: thesis: verum