let x, y, c be object ; :: 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 S2 = 1GateCircStr (<*y,c*>,'&');

set A2 = 1GateCircuit (y,c,'&');

reconsider yy = y, cc = c as Vertex of (1GateCircStr (<*y,c*>,'&')) by Th43;

reconsider v2 = [<*y,c*>,'&'] as Element of InnerVertices (1GateCircStr (<*y,c*>,'&')) by Th47;

set S1 = 1GateCircStr (<*x,y*>,'&');

set A1 = 1GateCircuit (x,y,'&');

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

A2: (1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')) = (1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*x,y*>,'&')) by CIRCCOMB:5, CIRCCOMB:47;

then A3: MajorityIStr (x,y,c) = (1GateCircStr (<*y,c*>,'&')) +* ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) by CIRCCOMB:6;

then reconsider v = v2 as Element of InnerVertices (MajorityIStr (x,y,c)) by Th21;

(1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&')) = (1GateCircuit (y,c,'&')) +* (1GateCircuit (x,y,'&')) by CIRCCOMB:22, CIRCCOMB:60;

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;

reconsider yy = yy, cc = cc as Vertex of (MajorityIStr (x,y,c)) by A3, Th20;

A5: dom s2 = the carrier of (1GateCircStr (<*y,c*>,'&')) by CIRCUIT1:3;

thus (Following s) . [<*y,c*>,'&'] = (Following s2) . v by A3, A4, CIRCCOMB:64

.= '&' . <*(s2 . yy),(s2 . cc)*> by Th48

.= '&' . <*(s . yy),(s2 . cc)*> by A5, FUNCT_1:47

.= '&' . <*(s . yy),(s . cc)*> by A5, FUNCT_1:47

.= a '&' b by A1, Def5 ; :: thesis: verum

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 S2 = 1GateCircStr (<*y,c*>,'&');

set A2 = 1GateCircuit (y,c,'&');

reconsider yy = y, cc = c as Vertex of (1GateCircStr (<*y,c*>,'&')) by Th43;

reconsider v2 = [<*y,c*>,'&'] as Element of InnerVertices (1GateCircStr (<*y,c*>,'&')) by Th47;

set S1 = 1GateCircStr (<*x,y*>,'&');

set A1 = 1GateCircuit (x,y,'&');

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

A2: (1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')) = (1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*x,y*>,'&')) by CIRCCOMB:5, CIRCCOMB:47;

then A3: MajorityIStr (x,y,c) = (1GateCircStr (<*y,c*>,'&')) +* ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) by CIRCCOMB:6;

then reconsider v = v2 as Element of InnerVertices (MajorityIStr (x,y,c)) by Th21;

(1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&')) = (1GateCircuit (y,c,'&')) +* (1GateCircuit (x,y,'&')) by CIRCCOMB:22, CIRCCOMB:60;

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;

reconsider yy = yy, cc = cc as Vertex of (MajorityIStr (x,y,c)) by A3, Th20;

A5: dom s2 = the carrier of (1GateCircStr (<*y,c*>,'&')) by CIRCUIT1:3;

thus (Following s) . [<*y,c*>,'&'] = (Following s2) . v by A3, A4, CIRCCOMB:64

.= '&' . <*(s2 . yy),(s2 . cc)*> by Th48

.= '&' . <*(s . yy),(s2 . cc)*> by A5, FUNCT_1:47

.= '&' . <*(s . yy),(s . cc)*> by A5, FUNCT_1:47

.= a '&' b by A1, Def5 ; :: thesis: verum