:: Introduction to Circuits, I
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received December 15, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users
begin
::---------------------------------------------------------------------------
:: Circuits
::---------------------------------------------------------------------------
definition
let
S
be non
empty
non
void
Circuit-like
ManySortedSign
;
mode
Circuit of
S
is
finite-yielding
MSAlgebra
over
S
;
end;
definition
let
IIG
be non
empty
non
void
Circuit-like
ManySortedSign
;
let
SCS
be
non-empty
Circuit
of
IIG
;
func
Set-Constants
SCS
->
ManySortedSet
of
SortsWithConstants
IIG
means
:
Def1
:
:: CIRCUIT1:def 1
for
x
being
Vertex
of
IIG
st
x
in
dom
it
holds
it
.
x
in
Constants
(
SCS
,
x
);
existence
ex
b
1
being
ManySortedSet
of
SortsWithConstants
IIG
st
for
x
being
Vertex
of
IIG
st
x
in
dom
b
1
holds
b
1
.
x
in
Constants
(
SCS
,
x
)
proof
end;
correctness
uniqueness
for
b
1
,
b
2
being
ManySortedSet
of
SortsWithConstants
IIG
st ( for
x
being
Vertex
of
IIG
st
x
in
dom
b
1
holds
b
1
.
x
in
Constants
(
SCS
,
x
) ) & ( for
x
being
Vertex
of
IIG
st
x
in
dom
b
2
holds
b
2
.
x
in
Constants
(
SCS
,
x
) ) holds
b
1
=
b
2
;
proof
end;
end;
::
deftheorem
Def1
defines
Set-Constants
CIRCUIT1:def 1 :
for
IIG
being non
empty
non
void
Circuit-like
ManySortedSign
for
SCS
being
non-empty
Circuit
of
IIG
for
b
3
being
ManySortedSet
of
SortsWithConstants
IIG
holds
(
b
3
=
Set-Constants
SCS
iff for
x
being
Vertex
of
IIG
st
x
in
dom
b
3
holds
b
3
.
x
in
Constants
(
SCS
,
x
) );
theorem
:: CIRCUIT1:1
for
IIG
being non
empty
non
void
Circuit-like
ManySortedSign
for
SCS
being
non-empty
Circuit
of
IIG
for
v
being
Vertex
of
IIG
for
e
being
Element
of the
Sorts
of
SCS
.
v
st
v
in
SortsWithConstants
IIG
&
e
in
Constants
(
SCS
,
v
) holds
(
Set-Constants
SCS
)
.
v
=
e
proof
end;
definition
let
IIG
be non
empty
non
void
Circuit-like
ManySortedSign
;
let
CS
be
Circuit
of
IIG
;
mode
InputFuncs of
CS
is
ManySortedFunction
of
(
InputVertices
IIG
)
-->
NAT
, the
Sorts
of
CS
|
(
InputVertices
IIG
)
;
end;
theorem
Th2
:
:: CIRCUIT1:2
for
IIG
being non
empty
non
void
Circuit-like
ManySortedSign
for
SCS
being
non-empty
Circuit
of
IIG
for
InpFs
being
InputFuncs
of
SCS
for
n
being
Element
of
NAT
st
IIG
is
with_input_V
holds
(
commute
InpFs
)
.
n
is
InputValues
of
SCS
proof
end;
definition
let
IIG
be non
empty
non
void
Circuit-like
ManySortedSign
;
assume
A1
:
IIG
is
with_input_V
;
let
SCS
be
non-empty
Circuit
of
IIG
;
let
InpFs
be
InputFuncs
of
SCS
;
let
n
be
Element
of
NAT
;
func
n
-th_InputValues
InpFs
->
InputValues
of
SCS
equals
:: CIRCUIT1:def 2
(
commute
InpFs
)
.
n
;
coherence
(
commute
InpFs
)
.
n
is
InputValues
of
SCS
by
A1
,
Th2
;
correctness
;
end;
::
deftheorem
defines
-th_InputValues
CIRCUIT1:def 2 :
for
IIG
being non
empty
non
void
Circuit-like
ManySortedSign
st
IIG
is
with_input_V
holds
for
SCS
being
non-empty
Circuit
of
IIG
for
InpFs
being
InputFuncs
of
SCS
for
n
being
Element
of
NAT
holds
n
-th_InputValues
InpFs
=
(
commute
InpFs
)
.
n
;
definition
let
IIG
be non
empty
non
void
Circuit-like
ManySortedSign
;
let
SCS
be
Circuit
of
IIG
;
mode
State of
SCS
is
Element
of
product
the
Sorts
of
SCS
;
end;
theorem
:: CIRCUIT1:3
for
IIG
being non
empty
non
void
Circuit-like
ManySortedSign
for
SCS
being
non-empty
Circuit
of
IIG
for
s
being
State
of
SCS
holds
dom
s
=
the
carrier
of
IIG
by
PARTFUN1:def 2
;
theorem
:: CIRCUIT1:4
for
IIG
being non
empty
non
void
Circuit-like
ManySortedSign
for
SCS
being
non-empty
Circuit
of
IIG
for
s
being
State
of
SCS
for
v
being
Vertex
of
IIG
holds
s
.
v
in
the
Sorts
of
SCS
.
v
proof
end;
definition
let
IIG
be non
empty
non
void
Circuit-like
ManySortedSign
;
let
SCS
be
non-empty
Circuit
of
IIG
;
let
s
be
State
of
SCS
;
let
o
be
OperSymbol
of
IIG
;
func
o
depends_on_in
s
->
Element
of
Args
(
o
,
SCS
)
equals
:: CIRCUIT1:def 3
s
*
(
the_arity_of
o
)
;
coherence
s
*
(
the_arity_of
o
)
is
Element
of
Args
(
o
,
SCS
)
proof
end;
correctness
;
end;
::
deftheorem
defines
depends_on_in
CIRCUIT1:def 3 :
for
IIG
being non
empty
non
void
Circuit-like
ManySortedSign
for
SCS
being
non-empty
Circuit
of
IIG
for
s
being
State
of
SCS
for
o
being
OperSymbol
of
IIG
holds
o
depends_on_in
s
=
s
*
(
the_arity_of
o
)
;
theorem
Th5
:
:: CIRCUIT1:5
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
SCS
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
,
w
being
Vertex
of
IIG
for
e1
being
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
v
for
q1
being
DTree-yielding
FinSequence
st
v
in
InnerVertices
IIG
&
e1
=
[
(
action_at
v
)
, the
carrier
of
IIG
]
-tree
q1
holds
for
k
being
Element
of
NAT
st
k
in
dom
q1
&
q1
.
k
in
the
Sorts
of
(
FreeEnv
SCS
)
.
w
holds
w
=
(
the_arity_of
(
action_at
v
)
)
/.
k
proof
end;
registration
let
IIG
be non
empty
non
void
Circuit-like
monotonic
ManySortedSign
;
let
SCS
be
non-empty
finite-yielding
MSAlgebra
over
IIG
;
let
v
be
Vertex
of
IIG
;
cluster
->
Relation-like
Function-like
non
empty
finite
for
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
v
;
coherence
for
b
1
being
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
v
holds
(
b
1
is
finite
& not
b
1
is
empty
&
b
1
is
Function-like
&
b
1
is
Relation-like
)
;
end;
registration
let
IIG
be non
empty
non
void
Circuit-like
monotonic
ManySortedSign
;
let
SCS
be
non-empty
finite-yielding
MSAlgebra
over
IIG
;
let
v
be
Vertex
of
IIG
;
cluster
->
DecoratedTree-like
for
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
v
;
coherence
for
b
1
being
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
v
holds
b
1
is
DecoratedTree-like
;
end;
theorem
Th6
:
:: CIRCUIT1:6
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
SCS
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
,
w
being
Vertex
of
IIG
for
e1
being
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
v
for
e2
being
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
w
for
q1
being
DTree-yielding
FinSequence
for
k1
being
Element
of
NAT
st
v
in
(
InnerVertices
IIG
)
\
(
SortsWithConstants
IIG
)
&
e1
=
[
(
action_at
v
)
, the
carrier
of
IIG
]
-tree
q1
&
k1
+
1
in
dom
q1
&
q1
.
(
k1
+
1
)
in
the
Sorts
of
(
FreeEnv
SCS
)
.
w
holds
e1
with-replacement
(
<*
k1
*>
,
e2
)
in
the
Sorts
of
(
FreeEnv
SCS
)
.
v
proof
end;
theorem
Th7
:
:: CIRCUIT1:7
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
being
Element
of
IIG
for
e
being
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
st 1
<
card
e
holds
ex
o
being
OperSymbol
of
IIG
st
e
.
{}
=
[
o
, the
carrier
of
IIG
]
proof
end;
theorem
:: CIRCUIT1:8
for
IIG
being non
empty
non
void
Circuit-like
ManySortedSign
for
SCS
being
non-empty
Circuit
of
IIG
for
s
being
State
of
SCS
for
o
being
OperSymbol
of
IIG
holds
(
Den
(
o
,
SCS
)
)
.
(
o
depends_on_in
s
)
in
the
Sorts
of
SCS
.
(
the_result_sort_of
o
)
proof
end;
theorem
Th9
:
:: CIRCUIT1:9
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
Circuit
of
IIG
for
v
being
Vertex
of
IIG
for
e
being
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
st
e
.
{}
=
[
(
action_at
v
)
, the
carrier
of
IIG
]
holds
ex
p
being
DTree-yielding
FinSequence
st
e
=
[
(
action_at
v
)
, the
carrier
of
IIG
]
-tree
p
proof
end;
begin
registration
let
IIG
be non
empty
non
void
monotonic
ManySortedSign
;
let
A
be
non-empty
finite-yielding
MSAlgebra
over
IIG
;
let
v
be
SortSymbol
of
IIG
;
cluster
the
Sorts
of
(
FreeEnv
A
)
.
v
->
finite
;
coherence
the
Sorts
of
(
FreeEnv
A
)
.
v
is
finite
proof
end;
end;
defpred
S
1
[
set
]
means
verum;
definition
let
IIG
be non
empty
non
void
Circuit-like
monotonic
ManySortedSign
;
let
A
be
non-empty
finite-yielding
MSAlgebra
over
IIG
;
let
v
be
SortSymbol
of
IIG
;
func
size
(
v
,
A
)
->
Nat
means
:
Def4
:
:: CIRCUIT1:def 4
ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
card
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
it
=
max
s
);
existence
ex
b
1
being
Nat
ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
card
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
b
1
=
max
s
)
proof
end;
correctness
uniqueness
for
b
1
,
b
2
being
Nat
st ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
card
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
b
1
=
max
s
) & ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
card
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
b
2
=
max
s
) holds
b
1
=
b
2
;
;
end;
::
deftheorem
Def4
defines
size
CIRCUIT1:def 4 :
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
being
SortSymbol
of
IIG
for
b
4
being
Nat
holds
(
b
4
=
size
(
v
,
A
) iff ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
card
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
b
4
=
max
s
) );
theorem
Th10
:
:: CIRCUIT1:10
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
being
Element
of
IIG
holds
(
size
(
v
,
A
)
=
1 iff
v
in
(
InputVertices
IIG
)
\/
(
SortsWithConstants
IIG
)
)
proof
end;
theorem
:: CIRCUIT1:11
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
SCS
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
,
w
being
Vertex
of
IIG
for
e1
being
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
v
for
e2
being
Element
of the
Sorts
of
(
FreeEnv
SCS
)
.
w
for
q1
being
DTree-yielding
FinSequence
st
v
in
(
InnerVertices
IIG
)
\
(
SortsWithConstants
IIG
)
&
card
e1
=
size
(
v
,
SCS
) &
e1
=
[
(
action_at
v
)
, the
carrier
of
IIG
]
-tree
q1
&
e2
in
rng
q1
holds
card
e2
=
size
(
w
,
SCS
)
proof
end;
theorem
Th12
:
:: CIRCUIT1:12
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
being
Vertex
of
IIG
for
e
being
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
st
v
in
(
InnerVertices
IIG
)
\
(
SortsWithConstants
IIG
)
&
card
e
=
size
(
v
,
A
) holds
ex
q
being
DTree-yielding
FinSequence
st
e
=
[
(
action_at
v
)
, the
carrier
of
IIG
]
-tree
q
proof
end;
theorem
:: CIRCUIT1:13
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
being
Vertex
of
IIG
for
e
being
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
st
v
in
(
InnerVertices
IIG
)
\
(
SortsWithConstants
IIG
)
&
card
e
=
size
(
v
,
A
) holds
ex
o
being
OperSymbol
of
IIG
st
e
.
{}
=
[
o
, the
carrier
of
IIG
]
proof
end;
definition
let
S
be non
empty
non
void
ManySortedSign
;
let
A
be
non-empty
finite-yielding
MSAlgebra
over
S
;
let
v
be
SortSymbol
of
S
;
let
e
be
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
;
func
depth
e
->
Element
of
NAT
means
:
Def5
:
:: CIRCUIT1:def 5
ex
e9
being
Element
of the
Sorts
of
(
FreeMSA
the
Sorts
of
A
)
.
v
st
(
e
=
e9
&
it
=
depth
e9
);
existence
ex
b
1
being
Element
of
NAT
ex
e9
being
Element
of the
Sorts
of
(
FreeMSA
the
Sorts
of
A
)
.
v
st
(
e
=
e9
&
b
1
=
depth
e9
)
proof
end;
correctness
uniqueness
for
b
1
,
b
2
being
Element
of
NAT
st ex
e9
being
Element
of the
Sorts
of
(
FreeMSA
the
Sorts
of
A
)
.
v
st
(
e
=
e9
&
b
1
=
depth
e9
) & ex
e9
being
Element
of the
Sorts
of
(
FreeMSA
the
Sorts
of
A
)
.
v
st
(
e
=
e9
&
b
2
=
depth
e9
) holds
b
1
=
b
2
;
;
end;
::
deftheorem
Def5
defines
depth
CIRCUIT1:def 5 :
for
S
being non
empty
non
void
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
S
for
v
being
SortSymbol
of
S
for
e
being
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
for
b
5
being
Element
of
NAT
holds
(
b
5
=
depth
e
iff ex
e9
being
Element
of the
Sorts
of
(
FreeMSA
the
Sorts
of
A
)
.
v
st
(
e
=
e9
&
b
5
=
depth
e9
) );
theorem
Th14
:
:: CIRCUIT1:14
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
,
w
being
Element
of
IIG
st
v
in
InnerVertices
IIG
&
w
in
rng
(
the_arity_of
(
action_at
v
)
)
holds
size
(
w
,
A
)
<
size
(
v
,
A
)
proof
end;
theorem
Th15
:
:: CIRCUIT1:15
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
being
SortSymbol
of
IIG
holds
size
(
v
,
A
)
>
0
proof
end;
theorem
:: CIRCUIT1:16
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
Circuit
of
IIG
for
v
being
Vertex
of
IIG
for
e
being
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
for
p
being
DTree-yielding
FinSequence
st
v
in
InnerVertices
IIG
&
e
=
[
(
action_at
v
)
, the
carrier
of
IIG
]
-tree
p
& ( for
k
being
Element
of
NAT
st
k
in
dom
p
holds
ex
ek
being
Element
of the
Sorts
of
(
FreeEnv
A
)
.
(
(
the_arity_of
(
action_at
v
)
)
/.
k
)
st
(
ek
=
p
.
k
&
card
ek
=
size
(
(
(
the_arity_of
(
action_at
v
)
)
/.
k
)
,
A
) ) ) holds
card
e
=
size
(
v
,
A
)
proof
end;
begin
definition
let
S
be non
empty
non
void
monotonic
ManySortedSign
;
let
A
be
non-empty
finite-yielding
MSAlgebra
over
S
;
let
v
be
SortSymbol
of
S
;
func
depth
(
v
,
A
)
->
Nat
means
:
Def6
:
:: CIRCUIT1:def 6
ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
depth
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
it
=
max
s
);
existence
ex
b
1
being
Nat
ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
depth
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
b
1
=
max
s
)
proof
end;
correctness
uniqueness
for
b
1
,
b
2
being
Nat
st ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
depth
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
b
1
=
max
s
) & ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
depth
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
b
2
=
max
s
) holds
b
1
=
b
2
;
;
end;
::
deftheorem
Def6
defines
depth
CIRCUIT1:def 6 :
for
S
being non
empty
non
void
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
S
for
v
being
SortSymbol
of
S
for
b
4
being
Nat
holds
(
b
4
=
depth
(
v
,
A
) iff ex
s
being non
empty
finite
Subset
of
NAT
st
(
s
=
{
(
depth
t
)
where
t
is
Element
of the
Sorts
of
(
FreeEnv
A
)
.
v
: verum
}
&
b
4
=
max
s
) );
definition
let
IIG
be non
empty
finite
non
void
Circuit-like
monotonic
ManySortedSign
;
let
A
be
non-empty
Circuit
of
IIG
;
func
depth
A
->
Nat
means
:
Def7
:
:: CIRCUIT1:def 7
ex
Ds
being non
empty
finite
Subset
of
NAT
st
(
Ds
=
{
(
depth
(
v
,
A
)
)
where
v
is
Element
of
IIG
:
v
in
the
carrier
of
IIG
}
&
it
=
max
Ds
);
existence
ex
b
1
being
Nat
ex
Ds
being non
empty
finite
Subset
of
NAT
st
(
Ds
=
{
(
depth
(
v
,
A
)
)
where
v
is
Element
of
IIG
:
v
in
the
carrier
of
IIG
}
&
b
1
=
max
Ds
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Nat
st ex
Ds
being non
empty
finite
Subset
of
NAT
st
(
Ds
=
{
(
depth
(
v
,
A
)
)
where
v
is
Element
of
IIG
:
v
in
the
carrier
of
IIG
}
&
b
1
=
max
Ds
) & ex
Ds
being non
empty
finite
Subset
of
NAT
st
(
Ds
=
{
(
depth
(
v
,
A
)
)
where
v
is
Element
of
IIG
:
v
in
the
carrier
of
IIG
}
&
b
2
=
max
Ds
) holds
b
1
=
b
2
;
end;
::
deftheorem
Def7
defines
depth
CIRCUIT1:def 7 :
for
IIG
being non
empty
finite
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
Circuit
of
IIG
for
b
3
being
Nat
holds
(
b
3
=
depth
A
iff ex
Ds
being non
empty
finite
Subset
of
NAT
st
(
Ds
=
{
(
depth
(
v
,
A
)
)
where
v
is
Element
of
IIG
:
v
in
the
carrier
of
IIG
}
&
b
3
=
max
Ds
) );
theorem
:: CIRCUIT1:17
for
IIG
being non
empty
finite
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
Circuit
of
IIG
for
v
being
Vertex
of
IIG
holds
depth
(
v
,
A
)
<=
depth
A
proof
end;
theorem
Th18
:
:: CIRCUIT1:18
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
Circuit
of
IIG
for
v
being
Vertex
of
IIG
holds
(
depth
(
v
,
A
)
=
0
iff (
v
in
InputVertices
IIG
or
v
in
SortsWithConstants
IIG
) )
proof
end;
theorem
:: CIRCUIT1:19
for
IIG
being non
empty
non
void
Circuit-like
monotonic
ManySortedSign
for
A
being
non-empty
finite-yielding
MSAlgebra
over
IIG
for
v
,
v1
being
SortSymbol
of
IIG
st
v
in
InnerVertices
IIG
&
v1
in
rng
(
the_arity_of
(
action_at
v
)
)
holds
depth
(
v1
,
A
)
<
depth
(
v
,
A
)
proof
end;
:: Circuits
::---------------------------------------------------------------------------