:: CIRCUIT1 semantic presentation

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
mode Circuit of a₁ is locally-finite MSAlgebra of a₁;

end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
func Set-Constants c₂ -> ManySortedSet of SortsWithConstants a₁ means :Def1: :: CIRCUIT1:def 1
for b₁ being Vertex of a₁ st b₁ in dom a₃ holds
a₃ . b₁ in Constants a₂,b₁;
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def1 defines Set-Constants CIRCUIT1:def 1 :

theorem Th1: :: CIRCUIT1:1

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being Vertex of b₁
for b₄ being Element of the Sorts of b₂ . b₃ st b₃ in SortsWithConstants b₁ & b₄ in Constants b₂,b₃ holds
(Set-Constants b₂) . b₃ = b₄

proof end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be Circuit of c₁;
mode InputFuncs of a₂ is ManySortedFunction of (InputVertices a₁) --> NAT ,the Sorts of a₂ | (InputVertices a₁);

end;

theorem Th2: :: CIRCUIT1:2

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputFuncs of b₂
for b₄ being Nat st b₁ is with_input_V holds
(commute b₃) . b₄ is InputValues of b₂

proof end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
assume E3: c₁ is with_input_V ;
let c₂ be non-empty Circuit of c₁;
let c₃ be InputFuncs of c₂;
let c₄ be Nat;
func c₄ -th_InputValues c₃ -> InputValues of a₂ equals :: CIRCUIT1:def 2
(commute a₃) . a₄;
coherence by E3, Th2;
correctness ;

end;

:: deftheorem Def2 defines -th_InputValues CIRCUIT1:def 2 :

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be Circuit of c₁;
mode State of a₂ is Element of product the Sorts of a₂;

end;

theorem Th3: :: CIRCUIT1:3

canceled;

theorem Th4: :: CIRCUIT1:4

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂ holds dom b₃ = the carrier of b₁

proof end;

theorem Th5: :: CIRCUIT1:5

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being Vertex of b₁ holds b₃ . b₄ in the Sorts of b₂ . b₄

proof end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be State of c₂;
let c₄ be OperSymbol of c₁;
func c₄ depends_on_in c₃ -> Element of Args a₄,a₂ equals :: CIRCUIT1:def 3
a₃ * (the_arity_of a₄);
coherence

proof end;

correctness ;

end;

:: deftheorem Def3 defines depends_on_in CIRCUIT1:def 3 :

theorem Th6: :: CIRCUIT1:6

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃, b₄ being Vertex of b₁
for b₅ being Element of the Sorts of (FreeEnv b₂) . b₃
for b₆ being DTree-yielding FinSequence st b₃ in InnerVertices b₁ & b₅ = [(action_at b₃),the carrier of b₁] -tree b₆ holds
for b₇ being Nat st b₇ in dom b₆ & b₆ . b₇ in the Sorts of (FreeEnv b₂) . b₄ holds
b₄ = (the_arity_of (action_at b₃)) /. b₇

proof end;

registration

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty locally-finite MSAlgebra of c₁;
let c₃ be Vertex of c₁;
cluster -> non empty Relation-like Function-like finite Element of the Sorts of (FreeEnv a₂) . a₃;
coherence

proof end;

end;

registration

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty locally-finite MSAlgebra of c₁;
let c₃ be Vertex of c₁;
cluster -> non empty Relation-like Function-like finite DecoratedTree-like Element of the Sorts of (FreeEnv a₂) . a₃;
coherence

proof end;

end;

theorem Th7: :: CIRCUIT1:7

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃, b₄ being Vertex of b₁
for b₅ being Element of the Sorts of (FreeEnv b₂) . b₃
for b₆ being Element of the Sorts of (FreeEnv b₂) . b₄
for b₇ being DTree-yielding FinSequence
for b₈ being Nat st b₃ in (InnerVertices b₁) \ (SortsWithConstants b₁) & b₅ = [(action_at b₃),the carrier of b₁] -tree b₇ & b₈ + 1 in dom b₇ & b₇ . (b₈ + 1) in the Sorts of (FreeEnv b₂) . b₄ holds
b₅ with-replacement <*b₈*>,b₆ in the Sorts of (FreeEnv b₂) . b₃

proof end;

theorem Th8: :: CIRCUIT1:8

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Element of b₁
for b₄ being Element of the Sorts of (FreeEnv b₂) . b₃ st 1 < card b₄ holds
ex b₅ being OperSymbol of b₁ st b₄ . {} = [b₅,the carrier of b₁]

proof end;

theorem Th9: :: CIRCUIT1:9

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being OperSymbol of b₁ holds (Den b₄,b₂) . (b₄ depends_on_in b₃) in the Sorts of b₂ . (the_result_sort_of b₄)

proof end;

theorem Th10: :: CIRCUIT1:10

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being Vertex of b₁
for b₄ being Element of the Sorts of (FreeEnv b₂) . b₃ st b₄ . {} = [(action_at b₃),the carrier of b₁] holds
ex b₅ being DTree-yielding FinSequence st b₄ = [(action_at b₃),the carrier of b₁] -tree b₅

proof end;

registration

let c₁ be non empty non void monotonic ManySortedSign ;
let c₂ be non-empty locally-finite MSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
cluster the Sorts of (FreeEnv a₂) . a₃ -> finite ;
coherence

proof end;

end;

defpred S₁[ set ] means verum;

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty locally-finite MSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
func size c₃,c₂ -> natural number means :Def4: :: CIRCUIT1:def 4
ex b₁ being non empty finite Subset of NAT st
( b₁ = { (card b₂) where B is Element of the Sorts of (FreeEnv a₂) . a₃ : verum } & a₄ = max b₁ );
existence

proof end;

correctness ;

end;

:: deftheorem Def4 defines size CIRCUIT1:def 4 :

theorem Th11: :: CIRCUIT1:11

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Element of b₁ holds
( size b₃,b₂ = 1 iff b₃ in (InputVertices b₁) \/ (SortsWithConstants b₁) )

proof end;

theorem Th12: :: CIRCUIT1:12

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃, b₄ being Vertex of b₁
for b₅ being Element of the Sorts of (FreeEnv b₂) . b₃
for b₆ being Element of the Sorts of (FreeEnv b₂) . b₄
for b₇ being DTree-yielding FinSequence st b₃ in (InnerVertices b₁) \ (SortsWithConstants b₁) & card b₅ = size b₃,b₂ & b₅ = [(action_at b₃),the carrier of b₁] -tree b₇ & b₆ in rng b₇ holds
card b₆ = size b₄,b₂

proof end;

theorem Th13: :: CIRCUIT1:13

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Vertex of b₁
for b₄ being Element of the Sorts of (FreeEnv b₂) . b₃ st b₃ in (InnerVertices b₁) \ (SortsWithConstants b₁) & card b₄ = size b₃,b₂ holds
ex b₅ being DTree-yielding FinSequence st b₄ = [(action_at b₃),the carrier of b₁] -tree b₅

proof end;

theorem Th14: :: CIRCUIT1:14

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being Vertex of b₁
for b₄ being Element of the Sorts of (FreeEnv b₂) . b₃ st b₃ in (InnerVertices b₁) \ (SortsWithConstants b₁) & card b₄ = size b₃,b₂ holds
ex b₅ being OperSymbol of b₁ st b₄ . {} = [b₅,the carrier of b₁]

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty locally-finite MSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
let c₄ be Element of the Sorts of (FreeEnv c₂) . c₃;
func depth c₄ -> Nat means :Def5: :: CIRCUIT1:def 5
ex b₁ being Element of the Sorts of (FreeMSA the Sorts of a₂) . a₃ st
( a₄ = b₁ & a₅ = depth b₁ );
existence

proof end;

correctness ;

end;

:: deftheorem Def5 defines depth CIRCUIT1:def 5 :

theorem Th15: :: CIRCUIT1:15

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃, b₄ being Element of b₁ st b₃ in InnerVertices b₁ & b₄ in rng (the_arity_of (action_at b₃)) holds
size b₄,b₂ < size b₃,b₂

proof end;

theorem Th16: :: CIRCUIT1:16

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃ being SortSymbol of b₁ holds size b₃,b₂ > 0

proof end;

theorem Th17: :: CIRCUIT1:17

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being Vertex of b₁
for b₄ being Element of the Sorts of (FreeEnv b₂) . b₃
for b₅ being DTree-yielding FinSequence st b₃ in InnerVertices b₁ & b₄ = [(action_at b₃),the carrier of b₁] -tree b₅ & ( for b₆ being Nat st b₆ in dom b₅ holds
ex b₇ being Element of the Sorts of (FreeEnv b₂) . ((the_arity_of (action_at b₃)) /. b₆) st
( b₇ = b₅ . b₆ & card b₇ = size ((the_arity_of (action_at b₃)) /. b₆),b₂ ) ) holds
card b₄ = size b₃,b₂

proof end;

definition

let c₁ be non empty non void monotonic ManySortedSign ;
let c₂ be non-empty locally-finite MSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
func depth c₃,c₂ -> natural number means :Def6: :: CIRCUIT1:def 6
ex b₁ being non empty finite Subset of NAT st
( b₁ = { (depth b₂) where B is Element of the Sorts of (FreeEnv a₂) . a₃ : verum } & a₄ = max b₁ );
existence

proof end;

correctness ;

end;

:: deftheorem Def6 defines depth CIRCUIT1:def 6 :

definition

let c₁ be non empty finite non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
func depth c₂ -> natural number means :Def7: :: CIRCUIT1:def 7
ex b₁ being non empty finite Subset of NAT st
( b₁ = { (depth b₂,a₂) where B is Element of a₁ : b₂ in the carrier of a₁ } & a₃ = max b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines depth CIRCUIT1:def 7 :

theorem Th18: :: CIRCUIT1:18

for b₁ being non empty finite non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being Vertex of b₁ holds depth b₃,b₂ <= depth b₂

proof end;

theorem Th19: :: CIRCUIT1:19

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being Vertex of b₁ holds
( depth b₃,b₂ = 0 iff ( b₃ in InputVertices b₁ or b₃ in SortsWithConstants b₁ ) )

proof end;

theorem Th20: :: CIRCUIT1:20

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty locally-finite MSAlgebra of b₁
for b₃, b₄ being SortSymbol of b₁ st b₃ in InnerVertices b₁ & b₄ in rng (the_arity_of (action_at b₃)) holds
depth b₄,b₂ < depth b₃,b₂

proof end;