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 . x & b = s . y holds
(Following s) . [<*x,y*>,'&'] = a '&' b
set xy = <*x,y*>;
set S1 = 1GateCircStr (<*x,y*>,'&');
set A1 = 1GateCircuit (x,y,'&');
reconsider xx = x, yy = y as Vertex of (1GateCircStr (<*x,y*>,'&')) by Th43;
reconsider v1 = [<*x,y*>,'&'] as Element of InnerVertices (1GateCircStr (<*x,y*>,'&')) by Th47;
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 . x & b = s . y holds
(Following s) . [<*x,y*>,'&'] = a '&' b
let a, b be Element of BOOLEAN ; :: thesis: ( a = s . x & b = s . y implies (Following s) . [<*x,y*>,'&'] = a '&' b )
assume A1: ( a = s . x & b = s . y ) ; :: thesis: (Following s) . [<*x,y*>,'&'] = a '&' b
A2: MajorityICirc (x,y,c) = (1GateCircuit (x,y,'&')) +* ((1GateCircuit (y,c,'&')) +* (1GateCircuit (c,x,'&'))) by Th25;
then reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,'&')) as State of (1GateCircuit (x,y,'&')) by Th26;
A3: MajorityIStr (x,y,c) = (1GateCircStr (<*x,y*>,'&')) +* ((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) by CIRCCOMB:6;
then reconsider v = v1 as Element of InnerVertices (MajorityIStr (x,y,c)) by Th21;
reconsider xx = xx, yy = yy as Vertex of (MajorityIStr (x,y,c)) by A3, Th20;
A4: dom s1 = the carrier of (1GateCircStr (<*x,y*>,'&')) by CIRCUIT1:3;
thus (Following s) . [<*x,y*>,'&'] = (Following s1) . v by A3, A2, CIRCCOMB:64
.= '&' . <*(s1 . xx),(s1 . yy)*> by Th48
.= '&' . <*(s . xx),(s1 . yy)*> by A4, FUNCT_1:47
.= '&' . <*(s . xx),(s . yy)*> by A4, FUNCT_1:47
.= a '&' b by A1, Def5 ; :: thesis: verum