A7: InnerVertices F₄((F₃() . 0),0) is Relation by A4;
defpred S₂[ Nat] means ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F₂($1) & S2 = F₂(($1 + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F₄((F₃() . $1),$1)) \ {(F₃() . $1)}) & F₃() . ($1 + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation );
A8: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
given S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign such that S1 = F₂(i) and
A9: S2 = F₂((i + 1)) and
InputVertices S2 = (InputVertices S1) \/ ((InputVertices F₄((F₃() . i),i)) \ {(F₃() . i)}) and
A10: F₃() . (i + 1) in InnerVertices S2 and
A11: InputVertices S2 is without_pairs and
A12: InnerVertices S2 is Relation ; :: thesis: S₂[i + 1]
A13: {(F₃() . (i + 1))} c= InnerVertices S2 by A10, ZFMISC_1:31;
take S2 ; :: thesis: ex S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S2 = F₂((i + 1)) & S2 = F₂(((i + 1) + 1)) & InputVertices S2 = (InputVertices S2) \/ ((InputVertices F₄((F₃() . (i + 1)),(i + 1))) \ {(F₃() . (i + 1))}) & F₃() . ((i + 1) + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation )
take S3 = S2 +* F₄((F₃() . (i + 1)),(i + 1)); :: thesis: ( S2 = F₂((i + 1)) & S3 = F₂(((i + 1) + 1)) & InputVertices S3 = (InputVertices S2) \/ ((InputVertices F₄((F₃() . (i + 1)),(i + 1))) \ {(F₃() . (i + 1))}) & F₃() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
thus ( S2 = F₂((i + 1)) & S3 = F₂(((i + 1) + 1)) ) by A6, A9; :: thesis: ( InputVertices S3 = (InputVertices S2) \/ ((InputVertices F₄((F₃() . (i + 1)),(i + 1))) \ {(F₃() . (i + 1))}) & F₃() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
A14: (InputVertices F₄((F₃() . (i + 1)),(i + 1))) \ {(F₃() . (i + 1))} is without_pairs by A5;
reconsider X1 = InputVertices S2, X2 = (InputVertices F₄((F₃() . (i + 1)),(i + 1))) \ {(F₃() . (i + 1))} as without_pairs set by A5, A11;
A15: InnerVertices F₄((F₃() . (i + 1)),(i + 1)) is Relation by A4;
thus InputVertices S3 = ((InputVertices S2) \ (InnerVertices F₄((F₃() . (i + 1)),(i + 1)))) \/ ((InputVertices F₄((F₃() . (i + 1)),(i + 1))) \ (InnerVertices S2)) by Th5, CIRCCOMB:47
.= (InputVertices S2) \/ ((InputVertices F₄((F₃() . (i + 1)),(i + 1))) \ (InnerVertices S2)) by A11, A15, Th6
.= (InputVertices S2) \/ ((InputVertices F₄((F₃() . (i + 1)),(i + 1))) \ {(F₃() . (i + 1))}) by A12, A14, A13, Th8 ; :: thesis: ( F₃() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
then A16: InputVertices S3 = X1 \/ X2 ;
A17: ( F₃() . ((i + 1) + 1) = F₅((F₃() . (i + 1)),(i + 1)) & F₅((F₃() . (i + 1)),(i + 1)) in InnerVertices F₄((F₃() . (i + 1)),(i + 1)) ) by A6, A9;
reconsider X1 = InnerVertices S2, X2 = InnerVertices F₄((F₃() . (i + 1)),(i + 1)) as Relation by A4, A12;
S2 tolerates F₄((F₃() . (i + 1)),(i + 1)) by CIRCCOMB:47;
then InnerVertices S3 = X1 \/ X2 by CIRCCOMB:11;
hence ( F₃() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation ) by A17, A16, XBOOLE_0:def 3; :: thesis: verum

end;

let n be Nat; :: thesis: ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F₂(n) & S2 = F₂((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F₄((F₃() . n),n)) \ {(F₃() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
A18: F₁() tolerates F₄((F₃() . 0),0) by CIRCCOMB:47;
A19: InputVertices (F₁() +* F₄((F₃() . 0),0)) = ((InputVertices F₁()) \ (InnerVertices F₄((F₃() . 0),0))) \/ ((InputVertices F₄((F₃() . 0),0)) \ (InnerVertices F₁())) by Th5, CIRCCOMB:47
.= (InputVertices F₁()) \/ ((InputVertices F₄((F₃() . 0),0)) \ (InnerVertices F₁())) by A2, A7, Th6 ;
A20: S₂[ 0 ]

proof

reconsider A = (InputVertices F₄((F₃() . 0),0)) \ {(F₃() . 0)}, B = InputVertices F₁() as without_pairs set by A2, A5;
take S0 = F₁(); :: thesis: ex S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S0 = F₂(0) & S2 = F₂((0 + 1)) & InputVertices S2 = (InputVertices S0) \/ ((InputVertices F₄((F₃() . 0),0)) \ {(F₃() . 0)}) & F₃() . (0 + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation )
take S1 = F₁() +* F₄((F₃() . 0),0); :: thesis: ( S0 = F₂(0) & S1 = F₂((0 + 1)) & InputVertices S1 = (InputVertices S0) \/ ((InputVertices F₄((F₃() . 0),0)) \ {(F₃() . 0)}) & F₃() . (0 + 1) in InnerVertices S1 & InputVertices S1 is without_pairs & InnerVertices S1 is Relation )
thus ( S0 = F₂(0) & S1 = F₂((0 + 1)) ) by A3, A6; :: thesis: ( InputVertices S1 = (InputVertices S0) \/ ((InputVertices F₄((F₃() . 0),0)) \ {(F₃() . 0)}) & F₃() . (0 + 1) in InnerVertices S1 & InputVertices S1 is without_pairs & InnerVertices S1 is Relation )
reconsider R1 = InnerVertices F₁(), R2 = InnerVertices F₄((F₃() . 0),0) as Relation by A1, A4;
for x being object st x in {(F₃() . 0)} holds
x in InnerVertices F₁() by A3, TARSKI:def 1;
then {(F₃() . 0)} c= InnerVertices F₁() by TARSKI:def 3;
then A21: InputVertices S1 = B \/ A by A1, A19, Th8;
( F₃() . (0 + 1) = F₅((F₃() . 0),0) & F₅((F₃() . 0),0) in R2 ) by A3, A6;
then F₃() . (0 + 1) in R1 \/ R2 by XBOOLE_0:def 3;
hence ( InputVertices S1 = (InputVertices S0) \/ ((InputVertices F₄((F₃() . 0),0)) \ {(F₃() . 0)}) & F₃() . (0 + 1) in InnerVertices S1 & InputVertices S1 is without_pairs & InnerVertices S1 is Relation ) by A18, A21, CIRCCOMB:11; :: thesis: verum

end;

A22: for i being Nat holds S₂[i] from NAT_1:sch 2(A20, A8);
then consider S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign such that
A23: S1 = F₂(n) and
A24: ( S2 = F₂((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F₄((F₃() . n),n)) \ {(F₃() . n)}) ) and
F₃() . (n + 1) in InnerVertices S2 and
InputVertices S2 is without_pairs and
InnerVertices S2 is Relation ;
take S1 ; :: thesis: ex S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F₂(n) & S2 = F₂((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F₄((F₃() . n),n)) \ {(F₃() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
take S2 ; :: thesis: ( S1 = F₂(n) & S2 = F₂((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F₄((F₃() . n),n)) \ {(F₃() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
thus ( S1 = F₂(n) & S2 = F₂((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F₄((F₃() . n),n)) \ {(F₃() . n)}) ) by A23, A24; :: thesis: ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs )

per cases ( n = 0 or ex i being Nat st n = i + 1 ) by NAT_1:6;

suppose n = 0 ; :: thesis: ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs )

hence ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) by A1, A2, A3, A23; :: thesis: verum

end;

suppose ex i being Nat st n = i + 1 ; :: thesis: ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs )

then consider i being Nat such that
A25: n = i + 1 ;
reconsider i = i as Nat ;
ex T1, T2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( T1 = F₂(i) & T2 = F₂((i + 1)) & InputVertices T2 = (InputVertices T1) \/ ((InputVertices F₄((F₃() . i),i)) \ {(F₃() . i)}) & F₃() . (i + 1) in InnerVertices T2 & InputVertices T2 is without_pairs & InnerVertices T2 is Relation ) by A22;
hence ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) by A23, A25; :: thesis: verum

end;

end;