:: Combining of Circuits
:: by Yatsuka Nakamura and Grzegorz Bancerek
::
:: Received May 11, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem :: CIRCCOMB:1
canceled;
theorem Th2: :: CIRCCOMB:2
theorem Th3: :: CIRCCOMB:3
theorem Th4: :: CIRCCOMB:4
theorem Th5: :: CIRCCOMB:5
theorem Th6: :: CIRCCOMB:6
:: deftheorem defines tolerates CIRCCOMB:def 1 :
:: deftheorem Def2 defines +* CIRCCOMB:def 2 :
theorem Th7: :: CIRCCOMB:7
theorem Th8: :: CIRCCOMB:8
theorem Th9: :: CIRCCOMB:9
theorem :: CIRCCOMB:10
theorem :: CIRCCOMB:11
theorem :: CIRCCOMB:12
theorem Th13: :: CIRCCOMB:13
theorem :: CIRCCOMB:14
theorem Th15: :: CIRCCOMB:15
theorem Th16: :: CIRCCOMB:16
theorem Th17: :: CIRCCOMB:17
theorem Th18: :: CIRCCOMB:18
theorem Th19: :: CIRCCOMB:19
theorem Th20: :: CIRCCOMB:20
theorem Th21: :: CIRCCOMB:21
:: deftheorem Def3 defines tolerates CIRCCOMB:def 3 :
:: deftheorem Def4 defines +* CIRCCOMB:def 4 :
theorem :: CIRCCOMB:22
theorem Th23: :: CIRCCOMB:23
theorem :: CIRCCOMB:24
theorem :: CIRCCOMB:25
theorem Th26: :: CIRCCOMB:26
theorem :: CIRCCOMB:27
theorem :: CIRCCOMB:28
theorem Th29: :: CIRCCOMB:29
theorem Th30: :: CIRCCOMB:30
theorem Th31: :: CIRCCOMB:31
theorem :: CIRCCOMB:32
theorem :: CIRCCOMB:33
theorem Th34: :: CIRCCOMB:34
theorem Th35: :: CIRCCOMB:35
theorem Th36: :: CIRCCOMB:36
theorem Th37: :: CIRCCOMB:37
theorem Th38: :: CIRCCOMB:38
theorem Th39: :: CIRCCOMB:39
theorem Th40: :: CIRCCOMB:40
theorem :: CIRCCOMB:41
theorem :: CIRCCOMB:42
definition
let f be
set ;
let p be
FinSequence;
let x be
set ;
func 1GateCircStr p,
f,
x -> non
void strict ManySortedSign means :
Def5:
:: CIRCCOMB:def 5
( 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: :: CIRCCOMB:43
theorem :: CIRCCOMB:44
theorem :: CIRCCOMB:45
definition
let f be
set ;
let p be
FinSequence;
func 1GateCircStr p,
f -> non
void strict ManySortedSign means :
Def6:
:: CIRCCOMB:def 6
( 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 :: CIRCCOMB:46
theorem Th47: :: CIRCCOMB:47
theorem Th48: :: CIRCCOMB:48
theorem Th49: :: CIRCCOMB:49
theorem :: CIRCCOMB:50
theorem Th51: :: CIRCCOMB:51
:: 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: :: CIRCCOMB:52
theorem :: CIRCCOMB:53
theorem Th54: :: CIRCCOMB:54
theorem Th55: :: CIRCCOMB:55
theorem Th56: :: CIRCCOMB:56
theorem Th57: :: CIRCCOMB:57
theorem Th58: :: CIRCCOMB:58
theorem Th59: :: CIRCCOMB:59
:: deftheorem Def12 defines FinSeqLen CIRCCOMB:def 12 :
definition
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 :: CIRCCOMB:def 13
( 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 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:
:: CIRCCOMB:def 14
( 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: :: CIRCCOMB:60
theorem Th61: :: CIRCCOMB:61
theorem Th62: :: CIRCCOMB:62
theorem :: CIRCCOMB:63
theorem :: CIRCCOMB:64
:: deftheorem Def15 defines Boolean CIRCCOMB:def 15 :
theorem Th65: :: CIRCCOMB:65
theorem :: CIRCCOMB:66
theorem Th67: :: CIRCCOMB:67
theorem Th68: :: CIRCCOMB:68
theorem :: CIRCCOMB:69
theorem Th70: :: CIRCCOMB:70
theorem Th71: :: CIRCCOMB:71
theorem :: CIRCCOMB:72