let x, y, c be set ; :: thesis: for s being State of (BorrowICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . x & b = s . c holds
(Following s) . [<*x,c*>,and2a] = ('not' a) '&' b
set xc = <*x,c*>;
set S3 = 1GateCircStr (<*x,c*>,and2a);
set A3 = 1GateCircuit (x,c,and2a);
set S = BorrowIStr (x,y,c);
set A = BorrowICirc (x,y,c);
set v3 = [<*x,c*>,and2a];
let s be State of (BorrowICirc (x,y,c)); :: thesis: for a, b being Element of BOOLEAN st a = s . x & b = s . c holds
(Following s) . [<*x,c*>,and2a] = ('not' a) '&' b
let a, b be Element of BOOLEAN ; :: thesis: ( a = s . x & b = s . c implies (Following s) . [<*x,c*>,and2a] = ('not' a) '&' b )
assume A1: ( a = s . x & b = s . c ) ; :: thesis: (Following s) . [<*x,c*>,and2a] = ('not' a) '&' b
reconsider xx = x, cc = c as Vertex of (1GateCircStr (<*x,c*>,and2a)) by FACIRC_1:43;
reconsider s3 = s | the carrier of (1GateCircStr (<*x,c*>,and2a)) as State of (1GateCircuit (x,c,and2a)) by FACIRC_1:26;
reconsider v3 = [<*x,c*>,and2a] as Element of InnerVertices (1GateCircStr (<*x,c*>,and2a)) by FACIRC_1:47;
reconsider v = v3 as Element of InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21;
A2: dom s3 = the carrier of (1GateCircStr (<*x,c*>,and2a)) by CIRCUIT1:3;
reconsider xx = xx, cc = cc as Vertex of (BorrowIStr (x,y,c)) by FACIRC_1:20;
thus (Following s) . [<*x,c*>,and2a] = (Following s3) . v by CIRCCOMB:64
.= and2a . <*(s3 . xx),(s3 . cc)*> by FACIRC_1:50
.= and2a . <*(s . xx),(s3 . cc)*> by A2, FUNCT_1:47
.= and2a . <*(s . xx),(s . cc)*> by A2, FUNCT_1:47
.= ('not' a) '&' b by A1, TWOSCOMP:def 2 ; :: thesis: verum