E:((n-1)(n-1)Prop). (EquivRel x,y:(n-1). x E y) & (x,y:(n-1). Dec(x E y)) (m:(n-1+1). m ~ (i,j:(n-1)//(i E j)))

nnProp

EquivRel x,y:n. x E y

x,y:n. Dec(x E y)

EquivRel x,y:(n-1). x E y

(n-1+1)

m(i,j:(n-1)//(i E j))

(i,j:(n-1)//(i E j))m

InvFuns(m; i,j:(n-1)//(i E j); f; g)

x:m. f(x) i,j:n//(i E j)

a:n. a E a

a,b:n. (a E b) (b E a)

a,b,c:n. (a E b) (b E c) (a E c)

x,y:i,j:n//(i E j). Dec(x = y)

(i,j:n//(i E j))(i,j:n//(i E j))

x,y:i,j:n//(i E j). (x Eb y) x = y

(k:(n-1). k E (n-1))

n-1 i,j:n//(i E j)

(m+1)(i,j:n//(i E j))

f1 = (x.if x=m n-1 else f(x) fi)

(i,j:n//(i E j))(m+1)

g1 = (x.if x Eb (n-1) m else g(x) fi)

i,j:n//(i E j)

(x Eb (n-1))

if g(x)=m n-1 else f(g(x)) fi = x i,j:n//(i E j)

RWO "17" 25
THEN
FwdThru Thm* n:{1...}, E:(nnProp). (EquivRel i,j:n. i E j) (x:i,j:n//(i E j). x = n-1 i,j:n//(i E j) x i,j:(n-1)//(i E j)) [25]

1	25. x = n-1 26. x i,j:(n-1)//(i E j) if g(x)=m n-1 else f(g(x)) fi = x i,j:n//(i E j)

About: