k:, c:((n-1)k). p:(k( List)). sum(||p(j)|| | j < k) = n-1 & (j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]) & (j:k, x:||p(j)||. (p(j))[x] < n-1 & c((p(j))[x]) = j)

k:, c:(nk). p:(k( List)). sum(||p(j)|| | j < k) = n & (j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]) & (j:k, x:||p(j)||. (p(j))[x] < n & c((p(j))[x]) = j)

(((RepeatFor 2 ((ParallelOp -1) THEN (Thin -3))) THEN ExRepD THEN (InstConcl [j.if c(n-1)=j [(n-1) / (p(j))] else p(j) fi])) THEN (Reduce 0) THEN (Analyze 0)) THENA ((RepeatFor 5 (Analyze THEN (Try (Complete Auto)))) THEN (GenConcl ((p1(j))[x] = a)) THEN (Try (Complete Auto)) THEN Analyze)

1	3. k: 4. c: nk 5. p: k( List) 6. sum(||p(j)|| | j < k) = n-1 7. j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y] 8. j:k, x:||p(j)||. (p(j))[x] < n-1 & c((p(j))[x]) = j sum(||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi|| | j < k) = n	8 steps
2	3. k: 4. c: nk 5. p: k( List) 6. sum(||p(j)|| | j < k) = n-1 7. j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y] 8. j:k, x:||p(j)||. (p(j))[x] < n-1 & c((p(j))[x]) = j (j:k, x,y:||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi||. x < y if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x] > if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[y]) & (j:k, x:||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi||. if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x] < n & c(if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]) = j)	14 steps

About: