let x1, x2, x3, x4, x5, x6, x7 be non pair set ; for s being State of (STC0ICirc (x1,x2,x3,x4,x5,x6,x7))
for a123, a567, a4 being Element of BOOLEAN st a123 = s . (GFA0AdderOutput (x1,x2,x3)) & a567 = s . (GFA0AdderOutput (x5,x6,x7)) & a4 = s . x4 holds
( (Following s) . [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] = a123 '&' a567 & (Following s) . [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] = a567 '&' a4 & (Following s) . [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] = a4 '&' a123 )
set S = STC0IStr (x1,x2,x3,x4,x5,x6,x7);
set C = STC0ICirc (x1,x2,x3,x4,x5,x6,x7);
set A1out = GFA0AdderOutput (x1,x2,x3);
set A2out = GFA0AdderOutput (x5,x6,x7);
set A1A2 = [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2];
set A2x4 = [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2];
set x4A1 = [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2];
let s be State of (STC0ICirc (x1,x2,x3,x4,x5,x6,x7)); for a123, a567, a4 being Element of BOOLEAN st a123 = s . (GFA0AdderOutput (x1,x2,x3)) & a567 = s . (GFA0AdderOutput (x5,x6,x7)) & a4 = s . x4 holds
( (Following s) . [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] = a123 '&' a567 & (Following s) . [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] = a567 '&' a4 & (Following s) . [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] = a4 '&' a123 )
let a123, a567, a4 be Element of BOOLEAN ; ( a123 = s . (GFA0AdderOutput (x1,x2,x3)) & a567 = s . (GFA0AdderOutput (x5,x6,x7)) & a4 = s . x4 implies ( (Following s) . [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] = a123 '&' a567 & (Following s) . [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] = a567 '&' a4 & (Following s) . [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] = a4 '&' a123 ) )
assume that
A1:
a123 = s . (GFA0AdderOutput (x1,x2,x3))
and
A2:
a567 = s . (GFA0AdderOutput (x5,x6,x7))
and
A3:
a4 = s . x4
; ( (Following s) . [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] = a123 '&' a567 & (Following s) . [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] = a567 '&' a4 & (Following s) . [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] = a4 '&' a123 )
A4:
dom s = the carrier of (STC0IStr (x1,x2,x3,x4,x5,x6,x7))
by CIRCUIT1:3;
A5:
GFA0AdderOutput (x1,x2,x3) in the carrier of (STC0IStr (x1,x2,x3,x4,x5,x6,x7))
by ThSTC0IS6;
A6:
GFA0AdderOutput (x5,x6,x7) in the carrier of (STC0IStr (x1,x2,x3,x4,x5,x6,x7))
by ThSTC0IS6;
A7:
InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) = the carrier' of (STC0IStr (x1,x2,x3,x4,x5,x6,x7))
by FACIRC_1:37;
hence (Following s) . [<*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>,and2] =
and2 . (s * <*(GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7))*>)
by ThSTC0IS7, FACIRC_1:35
.=
and2 . <*a123,a567*>
by A1, A2, A5, A6, A4, FINSEQ_2:125
.=
a123 '&' a567
by FACIRC_1:def 6
;
( (Following s) . [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] = a567 '&' a4 & (Following s) . [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] = a4 '&' a123 )
A8:
x4 in the carrier of (STC0IStr (x1,x2,x3,x4,x5,x6,x7))
by ThSTC0IS6;
thus (Following s) . [<*(GFA0AdderOutput (x5,x6,x7)),x4*>,and2] =
and2 . (s * <*(GFA0AdderOutput (x5,x6,x7)),x4*>)
by A7, ThSTC0IS7, FACIRC_1:35
.=
and2 . <*a567,a4*>
by A2, A3, A6, A8, A4, FINSEQ_2:125
.=
a567 '&' a4
by FACIRC_1:def 6
; (Following s) . [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] = a4 '&' a123
thus (Following s) . [<*x4,(GFA0AdderOutput (x1,x2,x3))*>,and2] =
and2 . (s * <*x4,(GFA0AdderOutput (x1,x2,x3))*>)
by A7, ThSTC0IS7, FACIRC_1:35
.=
and2 . <*a4,a123*>
by A3, A1, A8, A5, A4, FINSEQ_2:125
.=
a4 '&' a123
by FACIRC_1:def 6
; verum