:: CIRCUIT2 semantic presentation

Lemma1: for b₁ being set holds not b₁ in b₁
;

theorem Th1: :: CIRCUIT2:1

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being ManySortedFunction of (FreeMSA b₂),(FreeMSA b₂)
for b₄ being Function-yielding Function
for b₅ being SortSymbol of b₁
for b₆ being DTree-yielding FinSequence
for b₇ being Element of the Sorts of (FreeMSA b₂) . b₅ st b₅ in InnerVertices b₁ & b₇ = [(action_at b₅),the carrier of b₁] -tree b₆ & b₃ is_homomorphism FreeMSA b₂, FreeMSA b₂ & b₄ = b₃ * (the_arity_of (action_at b₅)) holds
ex b₈ being DTree-yielding FinSequence st
( b₈ = b₄ .. b₆ & (b₃ . b₅) . b₇ = [(action_at b₅),the carrier of b₁] -tree b₈ )

proof end;

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be State of c₂;
let c₄ be InputValues of c₂;
redefine func +* as c₃ +* c₄ -> State of a₂;
coherence

proof end;

end;

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be InputValues of c₂;
func Fix_inp c₃ -> ManySortedFunction of FreeGen the Sorts of a₂,the Sorts of (FreeEnv a₂) means :Def1: :: CIRCUIT2:def 1
for b₁ being Vertex of a₁ holds
( ( b₁ in InputVertices a₁ implies a₄ . b₁ = (FreeGen b₁,the Sorts of a₂) --> (root-tree [(a₃ . b₁),b₁]) ) & ( b₁ in SortsWithConstants a₁ implies a₄ . b₁ = (FreeGen b₁,the Sorts of a₂) --> (root-tree [(action_at b₁),the carrier of a₁]) ) & ( b₁ in (InnerVertices a₁) \ (SortsWithConstants a₁) implies a₄ . b₁ = id (FreeGen b₁,the Sorts of a₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Fix_inp CIRCUIT2:def 1 :

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be InputValues of c₂;
func Fix_inp_ext c₃ -> ManySortedFunction of (FreeEnv a₂),(FreeEnv a₂) means :Def2: :: CIRCUIT2:def 2
( a₄ is_homomorphism FreeEnv a₂, FreeEnv a₂ & Fix_inp a₃ c= a₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Fix_inp_ext CIRCUIT2:def 2 :

theorem Th2: :: CIRCUIT2:2

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputValues of b₂
for b₄ being Vertex of b₁
for b₅ being Element of the Sorts of (FreeEnv b₂) . b₄
for b₆ being set st b₄ in (InnerVertices b₁) \ (SortsWithConstants b₁) & b₅ = root-tree [b₆,b₄] holds
((Fix_inp_ext b₃) . b₄) . b₅ = b₅

proof end;

theorem Th3: :: CIRCUIT2:3

proof end;

theorem Th4: :: CIRCUIT2:4

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

proof end;

theorem Th5: :: CIRCUIT2:5

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputValues of b₂
for b₄ being Vertex of b₁
for b₅ being Element of the Sorts of (FreeEnv b₂) . b₄ st b₄ in SortsWithConstants b₁ holds
((Fix_inp_ext b₃) . b₄) . b₅ = root-tree [(action_at b₄),the carrier of b₁]

proof end;

theorem Th6: :: CIRCUIT2:6

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputValues of b₂
for b₄ being Vertex of b₁
for b₅, b₆ being Element of the Sorts of (FreeEnv b₂) . b₄
for b₇, b₈ being DecoratedTree st b₇ = b₅ & b₈ = b₆ & b₆ = ((Fix_inp_ext b₃) . b₄) . b₅ holds
dom b₇ = dom b₈

proof end;

theorem Th7: :: CIRCUIT2:7

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputValues of b₂
for b₄ being Vertex of b₁
for b₅, b₆ being Element of the Sorts of (FreeEnv b₂) . b₄ st b₆ = ((Fix_inp_ext b₃) . b₄) . b₅ holds
card b₅ = card b₆

proof end;

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be Vertex of c₁;
let c₄ be InputValues of c₂;
E11: FreeEnv c₂ = FreeMSA the Sorts of c₂ by MSAFREE2:def 8;
func IGTree c₃,c₄ -> Element of the Sorts of (FreeEnv a₂) . a₃ means :Def3: :: CIRCUIT2:def 3
ex b₁ being Element of the Sorts of (FreeEnv a₂) . a₃ st
( card b₁ = size a₃,a₂ & a₅ = ((Fix_inp_ext a₄) . a₃) . b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines IGTree CIRCUIT2:def 3 :

theorem Th8: :: CIRCUIT2:8

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 InputValues of b₂ holds IGTree b₃,b₄ = ((Fix_inp_ext b₄) . b₃) . (IGTree b₃,b₄)

proof end;

theorem Th9: :: CIRCUIT2:9

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 InputValues of b₂
for b₅ being DTree-yielding FinSequence st b₃ in InnerVertices b₁ & dom b₅ = dom (the_arity_of (action_at b₃)) & ( for b₆ being Nat st b₆ in dom b₅ holds
b₅ . b₆ = IGTree ((the_arity_of (action_at b₃)) /. b₆),b₄ ) holds
IGTree b₃,b₄ = [(action_at b₃),the carrier of b₁] -tree b₅

proof end;

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be Vertex of c₁;
let c₄ be InputValues of c₂;
func IGValue c₃,c₄ -> Element of the Sorts of a₂ . a₃ equals :: CIRCUIT2:def 4
((Eval a₂) . a₃) . (IGTree a₃,a₄);
coherence ;

end;

:: deftheorem Def4 defines IGValue CIRCUIT2:def 4 :

theorem Th10: :: CIRCUIT2: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 InputValues of b₂ st b₃ in InputVertices b₁ holds
IGValue b₃,b₄ = b₄ . b₃

proof end;

theorem Th11: :: CIRCUIT2:11

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 InputValues of b₂ st b₃ in SortsWithConstants b₁ holds
IGValue b₃,b₄ = (Set-Constants 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₂;
func Following c₃ -> State of a₂ means :Def5: :: CIRCUIT2:def 5
for b₁ being Vertex of a₁ holds
( ( b₁ in InputVertices a₁ implies a₄ . b₁ = a₃ . b₁ ) & ( b₁ in InnerVertices a₁ implies a₄ . b₁ = (Den (action_at b₁),a₂) . ((action_at b₁) depends_on_in a₃) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Following CIRCUIT2:def 5 :

theorem Th12: :: CIRCUIT2:12

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being InputValues of b₂ st b₄ c= b₃ holds
b₄ c= Following 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₂;
attr a₃ is stable means :Def6: :: CIRCUIT2:def 6
a₃ = Following a₃;

end;

:: deftheorem Def6 defines stable CIRCUIT2:def 6 :

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be State of c₂;
let c₄ be InputValues of c₂;
func Following c₃,c₄ -> State of a₂ equals :: CIRCUIT2:def 7
Following (a₃ +* a₄);
coherence ;

end;

:: deftheorem Def7 defines Following CIRCUIT2:def 7 :

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be InputFuncs of c₂;
let c₄ be State of c₂;
func InitialComp c₄,c₃ -> State of a₂ equals :: CIRCUIT2:def 8
(a₄ +* (0 -th_InputValues a₃)) +* (Set-Constants a₂);
coherence

proof end;

end;

:: deftheorem Def8 defines InitialComp CIRCUIT2:def 8 :

definition

let c₁ be non empty non void Circuit-like monotonic ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be InputFuncs of c₂;
let c₄ be State of c₂;
func Computation c₄,c₃ -> Function of NAT , product the Sorts of a₂ means :Def9: :: CIRCUIT2:def 9
( a₅ . 0 = InitialComp a₄,a₃ & ( for b₁ being Nat holds a₅ . (b₁ + 1) = Following (a₅ . b₁),((b₁ + 1) -th_InputValues a₃) ) );
correctness

proof end;

end;

:: deftheorem Def9 defines Computation CIRCUIT2:def 9 :

theorem Th13: :: CIRCUIT2:13

for b₁ being non empty non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being InputValues of b₂
for b₅ being Nat st ( for b₆ being Vertex of b₁ st depth b₆,b₂ <= b₅ holds
b₃ . b₆ = IGValue b₆,b₄ ) holds
for b₆ being Vertex of b₁ st depth b₆,b₂ <= b₅ + 1 holds
(Following b₃) . b₆ = IGValue b₆,b₄

proof end;

theorem Th14: :: CIRCUIT2:14

for b₁ being non empty finite non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputFuncs of b₂ st commute b₃ is constant & not InputVertices b₁ is empty holds
for b₄ being State of b₂
for b₅ being InputValues of b₂ st b₅ = (commute b₃) . 0 holds
for b₆ being Nat holds b₅ c= (Computation b₄,b₃) . b₆

proof end;

theorem Th15: :: CIRCUIT2:15

for b₁ being non empty finite non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputFuncs of b₂
for b₄ being State of b₂
for b₅ being Nat st commute b₃ is constant & not InputVertices b₁ is empty & (Computation b₄,b₃) . b₅ is stable holds
for b₆ being Nat st b₅ <= b₆ holds
(Computation b₄,b₃) . b₅ = (Computation b₄,b₃) . b₆

proof end;

theorem Th16: :: CIRCUIT2:16

proof end;

theorem Th17: :: CIRCUIT2:17

for b₁ being non empty finite non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputFuncs of b₂
for b₄ being InputValues of b₂ st commute b₃ is constant & not InputVertices b₁ is empty & b₄ = (commute b₃) . 0 holds
for b₅ being State of b₂
for b₆ being Vertex of b₁
for b₇ being Element of NAT st b₇ = depth b₂ holds
((Computation b₅,b₃) . b₇) . b₆ = IGValue b₆,b₄

proof end;

theorem Th18: :: CIRCUIT2:18

for b₁ being non empty finite non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputFuncs of b₂ st commute b₃ is constant & not InputVertices b₁ is empty holds
for b₄ being State of b₂
for b₅ being Element of NAT st b₅ = depth b₂ holds
(Computation b₄,b₃) . b₅ is stable

proof end;

theorem Th19: :: CIRCUIT2:19

for b₁ being non empty finite non void Circuit-like monotonic ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being InputFuncs of b₂ st commute b₃ is constant & not InputVertices b₁ is empty holds
for b₄, b₅ being State of b₂ holds (Computation b₄,b₃) . (depth b₂) = (Computation b₅,b₃) . (depth b₂)

proof end;