let x, y, c be set ; :: thesis: ( 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] ; :: thesis: for s being State of (BorrowCirc (x,y,c)) holds Following (s,2) is stable

let s be State of (BorrowCirc (x,y,c)); :: thesis: 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;

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] ; :: thesis: for s being State of (BorrowCirc (x,y,c)) holds Following (s,2) is stable

let s be State of (BorrowCirc (x,y,c)); :: thesis: 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 :: thesis: for a being object st a in the carrier of (BorrowStr (x,y,c)) holds

(Following (s,2)) . a = (Following (Following (s,2))) . a

hence
Following (s,2) = Following (Following (s,2))
by A4, A5, FUNCT_1:2; :: according to CIRCUIT2:def 6 :: thesis: verum(Following (s,2)) . a = (Following (Following (s,2))) . a

let a be object ; :: thesis: ( 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)) ; :: thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a

then 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 :: thesis: verum

end;assume A24: a in the carrier of (BorrowStr (x,y,c)) ; :: thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a

then 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 :: thesis: verum

proof
end;

per cases
( v in InputVertices (BorrowStr (x,y,c)) or v in InnerVertices (BorrowStr (x,y,c)) )
by A25, XBOOLE_0:def 3;

end;

suppose
v in InputVertices (BorrowStr (x,y,c))
; :: thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a

end;

end;

suppose
v in InnerVertices (BorrowStr (x,y,c))
; :: thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a

then
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; :: thesis: verum

end;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; :: thesis: verum