let x, y, c be set ; ( x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] implies for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable )
set S = MajorityStr (x,y,c);
assume that
A1:
x <> [<*y,c*>,'&']
and
A2:
y <> [<*c,x*>,'&']
and
A3:
c <> [<*x,y*>,'&']
; for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable
let s be State of (MajorityCirc (x,y,c)); Following (s,2) is stable
A4:
dom (Following (Following (s,2))) = the carrier of (MajorityStr (x,y,c))
by CIRCUIT1:3;
A5:
dom (Following (s,2)) = the carrier of (MajorityStr (x,y,c))
by CIRCUIT1:3;
reconsider xx = x, yy = y, cc = c as Vertex of (MajorityStr (x,y,c)) by FACIRC_1:72;
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)) . (MajorityOutput (x,y,c)) = (((s . xx) '&' (s . yy)) 'or' ((s . yy) '&' (s . cc))) 'or' ((s . cc) '&' (s . xx))
by A1, A2, A3, Lm4;
A10:
(Following (s,2)) . [<*x,y*>,'&'] = (s . xx) '&' (s . yy)
by A1, A2, A3, A8, Lm4;
A11:
(Following (s,2)) . [<*y,c*>,'&'] = (s . yy) '&' (s . cc)
by A1, A2, A3, A6, Lm4;
A12:
(Following (s,2)) . [<*c,x*>,'&'] = (s . cc) '&' (s . xx)
by A1, A2, A3, A7, Lm4;
A13:
Following (s,2) = Following (Following s)
by FACIRC_1:15;
A14:
InputVertices (MajorityStr (x,y,c)) = {x,y,c}
by A1, A2, A3, Th20;
then A15:
x in InputVertices (MajorityStr (x,y,c))
by ENUMSET1:def 1;
A16:
y in InputVertices (MajorityStr (x,y,c))
by A14, ENUMSET1:def 1;
A17:
c in InputVertices (MajorityStr (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 (MajorityStr (x,y,c)) holds
(Following (s,2)) . a = (Following (Following (s,2))) . alet a be
object ;
( a in the carrier of (MajorityStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )assume A24:
a in the
carrier of
(MajorityStr (x,y,c))
;
(Following (s,2)) . a = (Following (Following (s,2))) . athen reconsider v =
a as
Vertex of
(MajorityStr (x,y,c)) ;
A25:
v in (InputVertices (MajorityStr (x,y,c))) \/ (InnerVertices (MajorityStr (x,y,c)))
by A24, XBOOLE_1:45;
thus
(Following (s,2)) . a = (Following (Following (s,2))) . a
verumproof
per cases
( v in InputVertices (MajorityStr (x,y,c)) or v in InnerVertices (MajorityStr (x,y,c)) )
by A25, XBOOLE_0:def 3;
suppose
v in InnerVertices (MajorityStr (x,y,c))
;
(Following (s,2)) . a = (Following (Following (s,2))) . athen
v in {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))}
by Th19;
then
(
v in {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} or
v in {(MajorityOutput (x,y,c))} )
by XBOOLE_0:def 3;
then
(
v = [<*x,y*>,'&'] or
v = [<*y,c*>,'&'] or
v = [<*c,x*>,'&'] or
v = MajorityOutput (
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, Lm3, Th28;
verum end;
end; end;
hence
Following (s,2) = Following (Following (s,2))
by A4, A5, FUNCT_1:2; CIRCUIT2:def 6 verum