let x, y, c be set ; :: thesis: for s being State of (MajorityICirc x,y,c)
for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,'&' ] = a '&' b
set yc = <*y,c*>;
set S1 = 1GateCircStr <*x,y*>,'&' ;
set A1 = 1GateCircuit x,y,'&' ;
set S2 = 1GateCircStr <*y,c*>,'&' ;
set A2 = 1GateCircuit y,c,'&' ;
set S3 = 1GateCircStr <*c,x*>,'&' ;
set A3 = 1GateCircuit c,x,'&' ;
set S = MajorityIStr x,y,c;
set A = MajorityICirc x,y,c;
let s be State of (MajorityICirc x,y,c); :: thesis: for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,'&' ] = a '&' b
let a, b be Element of BOOLEAN ; :: thesis: ( a = s . y & b = s . c implies (Following s) . [<*y,c*>,'&' ] = a '&' b )
assume A1: ( a = s . y & b = s . c ) ; :: thesis: (Following s) . [<*y,c*>,'&' ] = a '&' b
reconsider v2 = [<*y,c*>,'&' ] as Element of InnerVertices (1GateCircStr <*y,c*>,'&' ) by Th47;
A2: ( MajorityIStr x,y,c = ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) +* (1GateCircStr <*c,x*>,'&' ) & (1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' ) = (1GateCircStr <*y,c*>,'&' ) +* (1GateCircStr <*x,y*>,'&' ) ) by CIRCCOMB:9, CIRCCOMB:55;
then A3: MajorityIStr x,y,c = (1GateCircStr <*y,c*>,'&' ) +* ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*c,x*>,'&' )) by CIRCCOMB:10;
then reconsider v = v2 as Element of InnerVertices (MajorityIStr x,y,c) by Th21;
( MajorityICirc x,y,c = ((1GateCircuit x,y,'&' ) +* (1GateCircuit y,c,'&' )) +* (1GateCircuit c,x,'&' ) & (1GateCircuit x,y,'&' ) +* (1GateCircuit y,c,'&' ) = (1GateCircuit y,c,'&' ) +* (1GateCircuit x,y,'&' ) ) by CIRCCOMB:26, CIRCCOMB:68;
then A4: MajorityICirc x,y,c = (1GateCircuit y,c,'&' ) +* ((1GateCircuit x,y,'&' ) +* (1GateCircuit c,x,'&' )) by A2, Th25;
then reconsider s2 = s | the carrier of (1GateCircStr <*y,c*>,'&' ) as State of (1GateCircuit y,c,'&' ) by Th26;
A5: dom s2 = the carrier of (1GateCircStr <*y,c*>,'&' ) by CIRCUIT1:4;
reconsider yy = y, cc = c as Vertex of (1GateCircStr <*y,c*>,'&' ) by Th43;
reconsider yy = yy, cc = cc as Vertex of (MajorityIStr x,y,c) by A3, Th20;
thus (Following s) . [<*y,c*>,'&' ] = (Following s2) . v by A3, A4, CIRCCOMB:72
.= '&' . <*(s2 . yy),(s2 . cc)*> by Th48
.= '&' . <*(s . yy),(s2 . cc)*> by A5, FUNCT_1:70
.= '&' . <*(s . yy),(s . cc)*> by A5, FUNCT_1:70
.= a '&' b by A1, Def6 ; :: thesis: verum