Write the following claims about the array `A[1 … n]`.
The first, second, and last element (exist and) are different from each other. array_claim A[1...n] n >= 2 /\ A[1] != A[2] != A[n] != A[1] <=> A[1] != A[2] != A[n] or
It is a palindrome (the same from right to left as from left to right). array_claim A[1...n] AA i; 1 <= i < n: A[i] = A[n-i+1] <=> AA i; 1 <= i < n: A[i] = A[n-i] or
Its smallest element (exists and) is unique. array_claim A[1...n] EE i; 1 <= i <= n: AA j; 1 <= j <= n: A[j] > A[i] \/ i=j <=> EE i; 1 <= i <= n: AA j; 1 <= j <= n: A[j] >= A[i] or
Fix the following solution to the previous problem with as small changes as you can. array_claim A[1...n] EE i; 1 <= i <= n: AA j; 1 <= j <= n: A[j] > A[i] \/ i=j <=> EE i; 1 <= i <= n: AA j; 1 <= j < i: A[j] > A[i] /\ AA j; i < j <= n: A[j] > A[i] or
Write as simple a predicate as you can that says the same as `AA h; 1 <= h <= n: EE k; h <= k <= n: A[k] > A[h]`. array_claim A[1...n] f_nodes 7 AA h; 1 <= h <= n: EE k; h <= k <= n: A[k] > A[h] <=> or
Farewell to arrays, now we study mathematical induction. We try to prove that if `x in RR ^^ x ≥ -1 ^^ n in ZZ ^^ n ≥ 1`, then `(1+x)^n >= 1 + n x`.
Write the base case. assume n >= 0 /\ x >= -1; hide_expr 1+x = >=`>=` hide_expr = 1 + x or
The induction assumption is `(1+x)^n >= 1 + n x`. What do we have to prove? assume n >= 0 /\ x >= -1; hide_expr (1+x)^(n+1) = (1+x)^n >=`>=` 1 + n x hide_expr = 1 + (n+1)x or