let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ( S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for v being Vertex of S holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) ) )
assume A1:
S = S1 +* S2
; for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for v being Vertex of S holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) )
let A1 be non-empty Circuit of S1; for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for v being Vertex of S holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) )
let A2 be non-empty Circuit of S2; for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for v being Vertex of S holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) )
let A be non-empty Circuit of S; ( A1 tolerates A2 & A = A1 +* A2 implies for s being State of A
for v being Vertex of S holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) ) )
assume that
A2:
S1 tolerates S2
and
A3:
the Sorts of A1 tolerates the Sorts of A2
and
A4:
the Charact of A1 tolerates the Charact of A2
and
A5:
A = A1 +* A2
; CIRCCOMB:def 3 for s being State of A
for v being Vertex of S holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) )
let s be State of A; for v being Vertex of S holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) )
let v be Vertex of S; ( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) )
hereby for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v
let s1 be
State of
A1;
( s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) implies (Following s) . v = (Following s1) . v )assume A6:
s1 = s | the
carrier of
S1
;
( ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) implies (Following s) . v = (Following s1) . v )A7:
now ( v in InnerVertices S1 implies (Following s) . v = (Following s1) . v )assume
v in InnerVertices S1
;
(Following s) . v = (Following s1) . vthen reconsider v1 =
v as
Element of
InnerVertices S1 ;
A8:
(Following s1) . v1 = (Den ((action_at v1),A1)) . ((action_at v1) depends_on_in s1)
by CIRCUIT2:def 5;
v1 in InnerVertices S
by A1, A2, Th17;
then A9:
(Following s) . v = (Den ((action_at v),A)) . ((action_at v) depends_on_in s)
by CIRCUIT2:def 5;
A10:
action_at v = action_at v1
by A1, A2, Th17;
then
Den (
(action_at v1),
A1)
= Den (
(action_at v),
A)
by A1, A3, A4, A5, Th28;
hence
(Following s) . v = (Following s1) . v
by A1, A2, A6, A10, A9, A8, Th30;
verum end; hence
( (
v in InnerVertices S1 or (
v in the
carrier of
S1 &
v in InputVertices S ) ) implies
(Following s) . v = (Following s1) . v )
by A7;
verum
end;
let s2 be State of A2; ( s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) implies (Following s) . v = (Following s2) . v )
assume A15:
s2 = s | the carrier of S2
; ( ( not v in InnerVertices S2 & not ( v in the carrier of S2 & v in InputVertices S ) ) or (Following s) . v = (Following s2) . v )
A16:
now ( v in InnerVertices S2 implies (Following s) . v = (Following s2) . v )assume
v in InnerVertices S2
;
(Following s) . v = (Following s2) . vthen reconsider v2 =
v as
Element of
InnerVertices S2 ;
A17:
(Following s2) . v2 = (Den ((action_at v2),A2)) . ((action_at v2) depends_on_in s2)
by CIRCUIT2:def 5;
v2 in InnerVertices S
by A1, Th15;
then A18:
(Following s) . v = (Den ((action_at v),A)) . ((action_at v) depends_on_in s)
by CIRCUIT2:def 5;
A19:
action_at v = action_at v2
by A1, Th15;
then
Den (
(action_at v2),
A2)
= Den (
(action_at v),
A)
by A1, A3, A5, Th27;
hence
(Following s) . v = (Following s2) . v
by A1, A15, A19, A18, A17, Th29;
verum end;
hence
( ( not v in InnerVertices S2 & not ( v in the carrier of S2 & v in InputVertices S ) ) or (Following s) . v = (Following s2) . v )
by A16; verum