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:3;
A5:
dom (Following (s,2)) = the carrier of (BorrowStr (x,y,c))
by CIRCUIT1:3;
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 for a being object st a in the carrier of (BorrowStr (x,y,c)) holds
(Following (s,2)) . a = (Following (Following (s,2))) . alet a be
object ;
( 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:2; CIRCUIT2:def 6 verum