A7: InnerVertices F4((F3() . 0),0) is Relation by A4;
defpred S2[ Nat] means ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F2($1) & S2 = F2(($1 + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . $1),$1)) \ {(F3() . $1)}) & F3() . ($1 + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation );
A8: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
given S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign such that S1 = F2(i) and
A9: S2 = F2((i + 1)) and
InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . i),i)) \ {(F3() . i)}) and
A10: F3() . (i + 1) in InnerVertices S2 and
A11: InputVertices S2 is without_pairs and
A12: InnerVertices S2 is Relation ; :: thesis: S2[i + 1]
A13: {(F3() . (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 = F2((i + 1)) & S2 = F2(((i + 1) + 1)) & InputVertices S2 = (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))}) & F3() . ((i + 1) + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation )
take S3 = S2 +* F4((F3() . (i + 1)),(i + 1)); :: thesis: ( S2 = F2((i + 1)) & S3 = F2(((i + 1) + 1)) & InputVertices S3 = (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))}) & F3() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
thus ( S2 = F2((i + 1)) & S3 = F2(((i + 1) + 1)) ) by A6, A9; :: thesis: ( InputVertices S3 = (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))}) & F3() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
A14: (InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))} is without_pairs by A5;
reconsider X1 = InputVertices S2, X2 = (InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))} as without_pairs set by A5, A11;
A15: InnerVertices F4((F3() . (i + 1)),(i + 1)) is Relation by A4;
thus InputVertices S3 = ((InputVertices S2) \ (InnerVertices F4((F3() . (i + 1)),(i + 1)))) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ (InnerVertices S2)) by Th5, CIRCCOMB:47
.= (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ (InnerVertices S2)) by A11, A15, Th6
.= (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))}) by A12, A14, A13, Th8 ; :: thesis: ( F3() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
then A16: InputVertices S3 = X1 \/ X2 ;
A17: ( F3() . ((i + 1) + 1) = F5((F3() . (i + 1)),(i + 1)) & F5((F3() . (i + 1)),(i + 1)) in InnerVertices F4((F3() . (i + 1)),(i + 1)) ) by A6, A9;
reconsider X1 = InnerVertices S2, X2 = InnerVertices F4((F3() . (i + 1)),(i + 1)) as Relation by A4, A12;
S2 tolerates F4((F3() . (i + 1)),(i + 1)) by CIRCCOMB:47;
then InnerVertices S3 = X1 \/ X2 by CIRCCOMB:11;
hence ( F3() . ((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 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
A18: F1() tolerates F4((F3() . 0),0) by CIRCCOMB:47;
A19: InputVertices (F1() +* F4((F3() . 0),0)) = ((InputVertices F1()) \ (InnerVertices F4((F3() . 0),0))) \/ ((InputVertices F4((F3() . 0),0)) \ (InnerVertices F1())) by Th5, CIRCCOMB:47
.= (InputVertices F1()) \/ ((InputVertices F4((F3() . 0),0)) \ (InnerVertices F1())) by A2, A7, Th6 ;
A20: S2[ 0 ]
proof
reconsider A = (InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}, B = InputVertices F1() as without_pairs set by A2, A5;
take S0 = F1(); :: thesis: ex S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S0 = F2(0) & S2 = F2((0 + 1)) & InputVertices S2 = (InputVertices S0) \/ ((InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}) & F3() . (0 + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation )
take S1 = F1() +* F4((F3() . 0),0); :: thesis: ( S0 = F2(0) & S1 = F2((0 + 1)) & InputVertices S1 = (InputVertices S0) \/ ((InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}) & F3() . (0 + 1) in InnerVertices S1 & InputVertices S1 is without_pairs & InnerVertices S1 is Relation )
thus ( S0 = F2(0) & S1 = F2((0 + 1)) ) by A3, A6; :: thesis: ( InputVertices S1 = (InputVertices S0) \/ ((InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}) & F3() . (0 + 1) in InnerVertices S1 & InputVertices S1 is without_pairs & InnerVertices S1 is Relation )
reconsider R1 = InnerVertices F1(), R2 = InnerVertices F4((F3() . 0),0) as Relation by A1, A4;
for x being object st x in {(F3() . 0)} holds
x in InnerVertices F1() by A3, TARSKI:def 1;
then {(F3() . 0)} c= InnerVertices F1() by TARSKI:def 3;
then A21: InputVertices S1 = B \/ A by A1, A19, Th8;
( F3() . (0 + 1) = F5((F3() . 0),0) & F5((F3() . 0),0) in R2 ) by A3, A6;
then F3() . (0 + 1) in R1 \/ R2 by XBOOLE_0:def 3;
hence ( InputVertices S1 = (InputVertices S0) \/ ((InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}) & F3() . (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 S2[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 = F2(n) and
A24: ( S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) ) and
F3() . (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 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
take S2 ; :: thesis: ( S1 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
thus ( S1 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . 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 = F2(i) & T2 = F2((i + 1)) & InputVertices T2 = (InputVertices T1) \/ ((InputVertices F4((F3() . i),i)) \ {(F3() . i)}) & F3() . (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;