let n be Nat; :: thesis: ( n > 0 implies card the InternalRel of (Necklace n) = 2 * (n - 1) )

deffunc H_{1}( Element of NAT ) -> Element of omega = $1 + 1;

deffunc H_{2}( Element of NAT ) -> Element of NAT = $1;

defpred S_{1}[ Element of NAT ] means $1 + 1 < n;

set A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ;

set B = { [H_{1}(i),H_{2}(i)] where i is Element of NAT : S_{1}[i] } ;

A1: { [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like_{1}(i),H_{2}(i)] where i is Element of NAT : S_{1}[i] }
by Th17;

assume A3: n > 0 ; :: thesis: card the InternalRel of (Necklace n) = 2 * (n - 1)

then n >= 0 + 1 by NAT_1:13;

then A4: n -' 1 = n - 1 by XREAL_1:233;

{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } = the InternalRel of (n -SuccRelStr) by Def6;

then A5: card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } = n - 1 by A3, Th15;

reconsider A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation by A1;

A6: A = { [H_{2}(i),H_{1}(i)] where i is Element of NAT : S_{1}[i] }
;

A7: A ~ = { [H_{1}(i),H_{2}(i)] where i is Element of NAT : S_{1}[i] }
from NECKLACE:sch 1(A6);

A8: A misses { [H_{1}(i),H_{2}(i)] where i is Element of NAT : S_{1}[i] }
_{1}(i),H_{2}(i)] where i is Element of NAT : S_{1}[i] } = n - 1
by A3, Th25;

then card the InternalRel of (Necklace n) = (card (n - 1)) +` (card (n - 1)) by A2, A5, A8, CARD_2:35

.= card ((n -' 1) + (n -' 1)) by A4, CARD_2:38

.= 2 * (n - 1) by A4 ;

hence card the InternalRel of (Necklace n) = 2 * (n - 1) ; :: thesis: verum

deffunc H

deffunc H

defpred S

set A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ;

set B = { [H

A1: { [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like

proof

A2:
the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [H
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or ex b_{1}, b_{2} being object st x = [b_{1},b_{2}] )

assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]

then ex i being Element of NAT st

( x = [i,(i + 1)] & i + 1 < n ) ;

hence ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]
; :: thesis: verum

end;assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: ex b

then ex i being Element of NAT st

( x = [i,(i + 1)] & i + 1 < n ) ;

hence ex b

assume A3: n > 0 ; :: thesis: card the InternalRel of (Necklace n) = 2 * (n - 1)

then n >= 0 + 1 by NAT_1:13;

then A4: n -' 1 = n - 1 by XREAL_1:233;

{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } = the InternalRel of (n -SuccRelStr) by Def6;

then A5: card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } = n - 1 by A3, Th15;

reconsider A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation by A1;

A6: A = { [H

A7: A ~ = { [H

A8: A misses { [H

proof

card { [H
assume
A meets { [H_{1}(i),H_{2}(i)] where i is Element of NAT : S_{1}[i] }
; :: thesis: contradiction

then consider x being object such that

A9: x in A and

A10: x in { [H_{1}(i),H_{2}(i)] where i is Element of NAT : S_{1}[i] }
by XBOOLE_0:3;

consider y, z being object such that

A11: x = [y,z] by A9, RELAT_1:def 1;

[z,y] in A by A7, A10, A11, RELAT_1:def 7;

then consider j being Element of NAT such that

A12: [z,y] = [j,(j + 1)] and

j + 1 < n ;

A13: ( z = j & y = j + 1 ) by A12, XTUPLE_0:1;

consider i being Element of NAT such that

A14: [y,z] = [i,(i + 1)] and

i + 1 < n by A9, A11;

( y = i & z = i + 1 ) by A14, XTUPLE_0:1;

hence contradiction by A13; :: thesis: verum

end;then consider x being object such that

A9: x in A and

A10: x in { [H

consider y, z being object such that

A11: x = [y,z] by A9, RELAT_1:def 1;

[z,y] in A by A7, A10, A11, RELAT_1:def 7;

then consider j being Element of NAT such that

A12: [z,y] = [j,(j + 1)] and

j + 1 < n ;

A13: ( z = j & y = j + 1 ) by A12, XTUPLE_0:1;

consider i being Element of NAT such that

A14: [y,z] = [i,(i + 1)] and

i + 1 < n by A9, A11;

( y = i & z = i + 1 ) by A14, XTUPLE_0:1;

hence contradiction by A13; :: thesis: verum

then card the InternalRel of (Necklace n) = (card (n - 1)) +` (card (n - 1)) by A2, A5, A8, CARD_2:35

.= card ((n -' 1) + (n -' 1)) by A4, CARD_2:38

.= 2 * (n - 1) by A4 ;

hence card the InternalRel of (Necklace n) = 2 * (n - 1) ; :: thesis: verum