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 . y holds
(Following s) . [<*x,y*>,and2a ] = ('not' a) '&' b
set xy = <*x,y*>;
set yc = <*y,c*>;
set xc = <*x,c*>;
set S1 = 1GateCircStr <*x,y*>,and2a ;
set A1 = 1GateCircuit x,y,and2a ;
set S2 = 1GateCircStr <*y,c*>,and2 ;
set A2 = 1GateCircuit y,c,and2 ;
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 v1 = [<*x,y*>,and2a ];
let s be State of (BorrowICirc x,y,c); :: thesis: for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,and2a ] = ('not' a) '&' b
let a, b be Element of BOOLEAN ; :: thesis: ( a = s . x & b = s . y implies (Following s) . [<*x,y*>,and2a ] = ('not' a) '&' b )
assume A1: ( a = s . x & b = s . y ) ; :: thesis: (Following s) . [<*x,y*>,and2a ] = ('not' a) '&' b
reconsider xx = x, yy = y as Vertex of (1GateCircStr <*x,y*>,and2a ) by FACIRC_1:43;
reconsider v1 = [<*x,y*>,and2a ] as Element of InnerVertices (1GateCircStr <*x,y*>,and2a ) by FACIRC_1:47;
A2: BorrowIStr x,y,c = (1GateCircStr <*x,y*>,and2a ) +* ((1GateCircStr <*y,c*>,and2 ) +* (1GateCircStr <*x,c*>,and2a )) by CIRCCOMB:10;
then reconsider v = v1 as Element of InnerVertices (BorrowIStr x,y,c) by FACIRC_1:21;
A3: BorrowICirc x,y,c = (1GateCircuit x,y,and2a ) +* ((1GateCircuit y,c,and2 ) +* (1GateCircuit x,c,and2a )) by FACIRC_1:25;
then reconsider s1 = s | the carrier of (1GateCircStr <*x,y*>,and2a ) as State of (1GateCircuit x,y,and2a ) by FACIRC_1:26;
reconsider xx = xx, yy = yy as Vertex of (BorrowIStr x,y,c) by A2, FACIRC_1:20;
A4: dom s1 = the carrier of (1GateCircStr <*x,y*>,and2a ) by CIRCUIT1:4;
thus (Following s) . [<*x,y*>,and2a ] = (Following s1) . v by A2, A3, CIRCCOMB:72
.= and2a . <*(s1 . xx),(s1 . yy)*> by FACIRC_1:50
.= and2a . <*(s . xx),(s1 . yy)*> by A4, FUNCT_1:70
.= and2a . <*(s . xx),(s . yy)*> by A4, FUNCT_1:70
.= ('not' a) '&' b by A1, TWOSCOMP:def 2 ; :: thesis: verum