let x, y, c be set ; ( x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] implies for s being State of (BorrowCirc x,y,c) holds Following s,2 is stable )
set S = BorrowStr x,y,c;
assume that
A1:
x <> [<*y,c*>,and2 ]
and
A2:
y <> [<*x,c*>,and2a ]
and
A3:
c <> [<*x,y*>,and2a ]
; for s being State of (BorrowCirc x,y,c) holds Following s,2 is stable
let s be State of (BorrowCirc x,y,c); Following s,2 is stable
A4:
dom (Following (Following s,2)) = the carrier of (BorrowStr x,y,c)
by CIRCUIT1:4;
A5:
dom (Following s,2) = the carrier of (BorrowStr x,y,c)
by CIRCUIT1:4;
reconsider xx = x, yy = y, cc = c as Vertex of (BorrowStr x,y,c) by FSCIRC_1:6;
set a1 = s . xx;
set a2 = s . yy;
set a3 = s . cc;
set ffs = Following s,2;
set fffs = Following (Following s,2);
A6:
s . xx = s . x
;
A7:
s . yy = s . y
;
A8:
s . cc = s . c
;
A9:
(Following s,2) . (BorrowOutput x,y,c) = ((('not' (s . xx)) '&' (s . yy)) 'or' ((s . yy) '&' (s . cc))) 'or' (('not' (s . xx)) '&' (s . cc))
by A1, A2, A3, Lm2;
A10:
(Following s,2) . [<*x,y*>,and2a ] = ('not' (s . xx)) '&' (s . yy)
by A1, A2, A3, A8, Lm2;
A11:
(Following s,2) . [<*y,c*>,and2 ] = (s . yy) '&' (s . cc)
by A1, A2, A3, A6, Lm2;
A12:
(Following s,2) . [<*x,c*>,and2a ] = ('not' (s . xx)) '&' (s . cc)
by A1, A2, A3, A7, Lm2;
A13:
Following s,2 = Following (Following s)
by FACIRC_1:15;
A14:
InputVertices (BorrowStr x,y,c) = {x,y,c}
by A1, A2, A3, Th15;
then A15:
x in InputVertices (BorrowStr x,y,c)
by ENUMSET1:def 1;
A16:
y in InputVertices (BorrowStr x,y,c)
by A14, ENUMSET1:def 1;
A17:
c in InputVertices (BorrowStr x,y,c)
by A14, ENUMSET1:def 1;
A18:
(Following s) . x = s . xx
by A15, CIRCUIT2:def 5;
A19:
(Following s) . y = s . yy
by A16, CIRCUIT2:def 5;
A20:
(Following s) . c = s . cc
by A17, CIRCUIT2:def 5;
A21:
(Following s,2) . x = s . xx
by A13, A15, A18, CIRCUIT2:def 5;
A22:
(Following s,2) . y = s . yy
by A13, A16, A19, CIRCUIT2:def 5;
A23:
(Following s,2) . c = s . cc
by A13, A17, A20, CIRCUIT2:def 5;
now let a be
set ;
( a in the carrier of (BorrowStr x,y,c) implies (Following s,2) . a = (Following (Following s,2)) . a )assume A24:
a in the
carrier of
(BorrowStr x,y,c)
;
(Following s,2) . a = (Following (Following s,2)) . athen reconsider v =
a as
Vertex of
(BorrowStr x,y,c) ;
A25:
v in (InputVertices (BorrowStr x,y,c)) \/ (InnerVertices (BorrowStr x,y,c))
by A24, XBOOLE_1:45;
thus
(Following s,2) . a = (Following (Following s,2)) . a
verumproof
per cases
( v in InputVertices (BorrowStr x,y,c) or v in InnerVertices (BorrowStr x,y,c) )
by A25, XBOOLE_0:def 3;
suppose
v in InnerVertices (BorrowStr x,y,c)
;
(Following s,2) . a = (Following (Following s,2)) . athen
v in {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)}
by Th14;
then
(
v in {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} or
v in {(BorrowOutput x,y,c)} )
by XBOOLE_0:def 3;
then
(
v = [<*x,y*>,and2a ] or
v = [<*y,c*>,and2 ] or
v = [<*x,c*>,and2a ] or
v = BorrowOutput x,
y,
c )
by ENUMSET1:def 1, TARSKI:def 1;
hence
(Following s,2) . a = (Following (Following s,2)) . a
by A9, A10, A11, A12, A21, A22, A23, Lm1, Th22;
verum end;
end; end;
hence
Following s,2 = Following (Following s,2)
by A4, A5, FUNCT_1:9; CIRCUIT2:def 6 verum