let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ( InputVertices S1 misses InnerVertices S2 & 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 s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume A1:
( InputVertices S1 misses InnerVertices S2 & 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 s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
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 s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
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 s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A be non-empty Circuit of S; ( A1 tolerates A2 & A = A1 +* A2 implies for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume that
A2:
A1 tolerates A2
and
A3:
A = A1 +* A2
; for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let s1 be State of A1; for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let s2 be State of A2; for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let s be State of A; ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable implies for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume that
A4:
s1 = s | the carrier of S1
and
A5:
s2 = s | the carrier of S2
and
A6:
s1 is stable
; for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
defpred S3[ Nat] means (Following (s,$1)) | the carrier of S2 = Following (s2,$1);
A7:
now for n being Nat st S3[n] holds
S3[n + 1]let n be
Nat;
( S3[n] implies S3[n + 1] )A8:
(
Following (
s,
(n + 1))
= Following (Following (s,n)) &
Following (Following (s2,n)) = Following (
s2,
(n + 1)) )
by FACIRC_1:12;
the
Sorts of
A1 tolerates the
Sorts of
A2
by A2, CIRCCOMB:def 3;
then reconsider Fs1 =
(Following (s,n)) | the
carrier of
S1 as
State of
A1 by A3, CIRCCOMB:26;
Following (
s1,
n)
= Fs1
by A1, A2, A3, A4, Th13;
then A9:
Fs1 is
stable
by A6, Th3;
assume
S3[
n]
;
S3[n + 1]hence
S3[
n + 1]
by A1, A2, A3, A8, A9, Th15;
verum end;
(Following (s,0)) | the carrier of S2 =
s2
by A5, FACIRC_1:11
.=
Following (s2,0)
by FACIRC_1:11
;
then A10:
S3[ 0 ]
;
thus
for n being Nat holds S3[n]
from NAT_1:sch 2(A10, A7); verum