begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem defines tolerates CIRCCOMB:def 1 :
:: deftheorem Def2 defines +* CIRCCOMB:def 2 :
theorem Th7:
theorem
theorem Th9:
theorem
theorem
theorem
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
:: deftheorem Def3 defines tolerates CIRCCOMB:def 3 :
:: deftheorem Def4 defines +* CIRCCOMB:def 4 :
theorem
theorem Th23:
theorem
theorem
theorem Th26:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem
begin
definition
let f be
set ;
let p be
FinSequence;
let x be
set ;
func 1GateCircStr p,
f,
x -> non
void strict ManySortedSign means :
Def5:
( the
carrier of
it = (rng p) \/ {x} & the
carrier' of
it = {[p,f]} & the
Arity of
it . [p,f] = p & the
ResultSort of
it . [p,f] = x );
existence
ex b1 being non void strict ManySortedSign st
( the carrier of b1 = (rng p) \/ {x} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = x )
uniqueness
for b1, b2 being non void strict ManySortedSign st the carrier of b1 = (rng p) \/ {x} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = x & the carrier of b2 = (rng p) \/ {x} & the carrier' of b2 = {[p,f]} & the Arity of b2 . [p,f] = p & the ResultSort of b2 . [p,f] = x holds
b1 = b2
end;
:: deftheorem Def5 defines 1GateCircStr CIRCCOMB:def 5 :
theorem Th43:
theorem
theorem
definition
let f be
set ;
let p be
FinSequence;
func 1GateCircStr p,
f -> non
void strict ManySortedSign means :
Def6:
( the
carrier of
it = (rng p) \/ {[p,f]} & the
carrier' of
it = {[p,f]} & the
Arity of
it . [p,f] = p & the
ResultSort of
it . [p,f] = [p,f] );
existence
ex b1 being non void strict ManySortedSign st
( the carrier of b1 = (rng p) \/ {[p,f]} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = [p,f] )
uniqueness
for b1, b2 being non void strict ManySortedSign st the carrier of b1 = (rng p) \/ {[p,f]} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = [p,f] & the carrier of b2 = (rng p) \/ {[p,f]} & the carrier' of b2 = {[p,f]} & the Arity of b2 . [p,f] = p & the ResultSort of b2 . [p,f] = [p,f] holds
b1 = b2
end;
:: deftheorem Def6 defines 1GateCircStr CIRCCOMB:def 6 :
theorem
theorem Th47:
theorem Th48:
theorem Th49:
theorem
canceled;
theorem Th51:
begin
:: deftheorem Def7 defines unsplit CIRCCOMB:def 7 :
:: deftheorem Def8 defines gate`1=arity CIRCCOMB:def 8 :
:: deftheorem Def9 defines gate`2isBoolean CIRCCOMB:def 9 :
:: deftheorem Def10 defines gate`2=den CIRCCOMB:def 10 :
:: deftheorem defines gate`2=den CIRCCOMB:def 11 :
theorem Th52:
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
begin
definition
canceled;let n be
Nat;
let X,
Y be non
empty set ;
let f be
Function of
(n -tuples_on X),
Y;
let p be
FinSeqLen of
n;
let x be
set ;
assume A1:
(
x in rng p implies
X = Y )
;
func 1GateCircuit p,
f,
x -> strict non-empty MSAlgebra of
1GateCircStr p,
f,
x means
( the
Sorts of
it = ((rng p) --> X) +* (x .--> Y) & the
Charact of
it . [p,f] = f );
existence
ex b1 being strict non-empty MSAlgebra of 1GateCircStr p,f,x st
( the Sorts of b1 = ((rng p) --> X) +* (x .--> Y) & the Charact of b1 . [p,f] = f )
uniqueness
for b1, b2 being strict non-empty MSAlgebra of 1GateCircStr p,f,x st the Sorts of b1 = ((rng p) --> X) +* (x .--> Y) & the Charact of b1 . [p,f] = f & the Sorts of b2 = ((rng p) --> X) +* (x .--> Y) & the Charact of b2 . [p,f] = f holds
b1 = b2
end;
:: deftheorem CIRCCOMB:def 12 :
canceled;
:: deftheorem defines 1GateCircuit CIRCCOMB:def 13 :
definition
let n be
Nat;
let X be non
empty set ;
let f be
Function of
(n -tuples_on X),
X;
let p be
FinSeqLen of
n;
func 1GateCircuit p,
f -> strict non-empty MSAlgebra of
1GateCircStr p,
f means :
Def14:
( the
Sorts of
it = the
carrier of
(1GateCircStr p,f) --> X & the
Charact of
it . [p,f] = f );
existence
ex b1 being strict non-empty MSAlgebra of 1GateCircStr p,f st
( the Sorts of b1 = the carrier of (1GateCircStr p,f) --> X & the Charact of b1 . [p,f] = f )
uniqueness
for b1, b2 being strict non-empty MSAlgebra of 1GateCircStr p,f st the Sorts of b1 = the carrier of (1GateCircStr p,f) --> X & the Charact of b1 . [p,f] = f & the Sorts of b2 = the carrier of (1GateCircStr p,f) --> X & the Charact of b2 . [p,f] = f holds
b1 = b2
end;
:: deftheorem Def14 defines 1GateCircuit CIRCCOMB:def 14 :
theorem Th60:
theorem Th61:
theorem Th62:
theorem
theorem
begin
:: deftheorem Def15 defines Boolean CIRCCOMB:def 15 :
theorem Th65:
theorem
theorem Th67:
theorem Th68:
theorem
theorem Th70:
theorem Th71:
theorem