consider A being Circuit of S such that
A1:
( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den )
by Def9;
A2:
dom the Sorts of A = the carrier of S
by PARTFUN1:def 4;
set B = MSAlgebra(# the Sorts of A,the Charact of A #);
the Sorts of A is finite-yielding
by MSAFREE2:def 11;
then reconsider B = MSAlgebra(# the Sorts of A,the Charact of A #) as Circuit of S by MSAFREE2:def 11;
for g being set st g in the carrier' of S holds
g = [(g `1 ),(the Charact of B . g)]
by A1, CIRCCOMB:def 10;
then
( B is gate`2=den & not the Sorts of B is empty & the Sorts of B is constant & the_value_of the Sorts of B = X )
by A1, CIRCCOMB:def 10;
then reconsider B = B as Circuit of X,S by Def10;
take
B
; :: thesis: ( B is strict & B is one-gate )
consider Y being non empty finite set , n being Element of NAT , p being FinSeqLen of , f being Function of (n -tuples_on Y),Y such that
A3:
S = 1GateCircStr p,f
by Def6;
set C = 1GateCircuit p,f;
set g = [p,f];
[p,f] in {[p,f]}
by TARSKI:def 1;
then A4:
[p,f] in the carrier' of S
by A3, CIRCCOMB:def 6;
then A5:
[p,f] = [([p,f] `1 ),(the Charact of B . [p,f])]
by CIRCCOMB:def 10;
A6:
[p,f] = [([p,f] `1 ),(the Charact of (1GateCircuit p,f) . [p,f])]
by A3, A4, CIRCCOMB:def 10;
dom (the Charact of B . [p,f]) = dom f
by A5, ZFMISC_1:33;
then A7:
dom (the Charact of B . [p,f]) = n -tuples_on Y
by FUNCT_2:def 1;
dom the ResultSort of S = the carrier' of S
by FUNCT_2:def 1;
then A8:
(the Sorts of B * the ResultSort of S) . [p,f] = the Sorts of B . (the ResultSort of S . [p,f])
by A4, FUNCT_1:23;
consider b being set such that
A9:
( b in dom the Sorts of B & X = the Sorts of B . b )
by A1, FUNCT_1:def 18;
A10:
the Sorts of B = the carrier of S --> X
by A1, A2, FUNCOP_1:95;
the ResultSort of S . [p,f] in the carrier of S
by A4, FUNCT_2:7;
then
the ResultSort of S . [p,f] in dom the Sorts of B
by PARTFUN1:def 4;
then A11:
the Sorts of B . (the ResultSort of S . [p,f]) = X
by A1, A9, FUNCT_1:def 16;
the Charact of B . [p,f] is Function of (((the Sorts of B # ) * the Arity of S) . [p,f]),((the Sorts of B * the ResultSort of S) . [p,f])
by A4, PBOOLE:def 18;
then A12:
dom (the Charact of B . [p,f]) = ((the Sorts of B # ) * the Arity of S) . [p,f]
by A8, A11, FUNCT_2:def 1;
A13:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
the Arity of S . [p,f] in the carrier of S *
by A4, FUNCT_2:7;
then reconsider Ag = the Arity of S . [p,f] as FinSequence of the carrier of S by FINSEQ_1:def 11;
A14: dom (the Charact of B . [p,f]) =
(the Sorts of B # ) . Ag
by A4, A12, A13, FUNCT_1:23
.=
(len Ag) -tuples_on X
by A10, CIRCCOMB:6
;
per cases
( n <> 0 or n = 0 )
;
suppose A16:
n = 0
;
:: thesis: ( B is strict & B is one-gate )
the
Charact of
B . [p,f] is
Function of
(((the Sorts of B # ) * the Arity of S) . [p,f]),
((the Sorts of B * the ResultSort of S) . [p,f])
by A4, PBOOLE:def 18;
then A17:
rng (the Charact of B . [p,f]) c= (the Sorts of B * the ResultSort of S) . [p,f]
by RELAT_1:def 19;
n -tuples_on X =
{(<*> X)}
by A16, FINSEQ_2:112
.=
{(<*> Y)}
.=
n -tuples_on Y
by A16, FINSEQ_2:112
;
then A18:
dom f = n -tuples_on X
by FUNCT_2:def 1;
the
Charact of
B . [p,f] = f
by A5, ZFMISC_1:33;
then reconsider h =
f as
Function of
(n -tuples_on X),
X by A8, A11, A17, A18, FUNCT_2:4;
set D =
1GateCircuit p,
h;
A19:
[p,f] = [([p,f] `1 ),(the Charact of (1GateCircuit p,h) . [p,f])]
by A3, A4, CIRCCOMB:def 10;
A20:
the
Sorts of
B = the
Sorts of
(1GateCircuit p,h)
by A3, A10, CIRCCOMB:def 14;
hence
(
B is
strict &
B is
one-gate )
by A3, A20, PBOOLE:3;
:: thesis: verum