Teh­tä­vä:
Tau­lu­koi­ta kos­ke­via väit­tei­tä

Ly­hyt Math­Check-oh­je (uu­teen vä­li­leh­teen)

Tau­luk­ko A in­dek­soi­daan 1, …, n. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä A on kas­va­vas­sa jär­jes­tyk­ses­sä. ok_text Oi­kein! array_claim A[1...n] f_nodes 19 b_nodes 14 AA i; 1 <= i < n: A[i] <= A[i+1] <=>

tai

Tau­luk­ko C in­dek­soi­daan 0, …, k − 1. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä C on ai­dos­ti kas­va­vas­sa jär­jes­tyk­ses­sä. ok_text Oi­kein! array_claim C[0...k-1] f_nodes 19 b_nodes 14 AA i; 0 <= i < k-1: C[i] < C[i+1] <=>

tai

Tau­luk­ko H in­dek­soi­daan 0:sta al­kaen, ja sii­nä on l al­kio­ta. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä H:n si­säl­tö on pa­lindro­mi eli sama etu- ja ta­ka­pe­rin. Esi­mer­kik­si [1,2,2,1] on pa­lindro­mi, mut­ta [1,0,2,0] ei ole. ok_text Oi­kein! array_claim H[0...l-1] f_nodes 18 b_nodes 16 AA i; 0 <= i < l: H[i] = H[l-i-1] <=>

tai

Tau­luk­ko Δ (Math­Checkis­sä De) in­dek­soi­daan 0, …, i. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä Δ si­säl­tää lu­vun 2 ai­na­kin ker­ran. ok_text Oi­kein! array_claim DE[0...i] f_nodes 11 EE h; 0 <= h <= i: DE[h] = 2 <=>

tai

Tau­luk­ko u in­dek­soi­daan 2, …, n − 1. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä u si­säl­tää ai­na­kin kak­si eri­suur­ta al­kio­ta. ok_text Oi­kein! array_claim u[2...n-1] f_nodes 17 b_nodes 15 EE i: EE j; 2 <= i < j < n: u[i] != u[j] <=>

tai

Tau­luk­ko u in­dek­soi­daan 2, …, n − 1. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä u si­säl­tää ai­na­kin kak­si al­kio­ta. ok_text Oi­kein! array_claim u[2...n-1] f_nodes 3 n >= 4 <=>

tai

Tau­luk­ko b in­dek­soi­daan −1, …, m − 1. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä b:n en­sim­mäi­nen al­kio ei ole b:n pie­nin al­kio. ok_text Oi­kein! array_claim b[-1...m-1] f_nodes 16 b_nodes 13 EE i; 0 <= i < m: b[-1] > b[i] <=>

tai

Tau­luk­ko ξ (Math­Checkis­sä xi) in­dek­soi­daan 3:sta al­kaen, ja se si­säl­tää M al­kio­ta. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä ξ:n jo­kai­nen al­kio esiin­tyy ξ:ssä ai­na­kin kah­des­ti. ok_text Oi­kein! array_claim xi[3...M+2] f_nodes 40 b_nodes 27 AA z; 3 <= z < M+3: EE u; 3 <= u < M+3: u != z /\ xi[z] = xi[u] <=>

tai

Tau­luk­ko i in­dek­soi­daan 2:sta al­kaen, ja se si­säl­tää a + 1 al­kio­ta. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä jo­kin i:ssä esiin­ty­vä ar­vo esiin­tyy i:ssä vain ker­ran. ok_text Oi­kein! array_claim i[2...a+2] f_nodes 40 b_nodes 27 EE k; 2 <= k <= a+2: AA h; 2 <= h <= a+2 /\ h != k: i[k] != i[h] <=>

tai

Tau­luk­ko x in­dek­soi­daan −5, …, a. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä x:n pai­kas­sa −3 on lu­ku 2. ok_text Oi­kein! array_claim x[-5...a] f_nodes 20 b_nodes 10 a >= -3 /\ x[-3] = 2 <=>

tai

Tau­luk­ko Γ (Math­Checkis­sä Ga) in­dek­soi­daan −2, …, g. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä Γ:n en­sim­mäi­nen ja vii­mei­nen al­kio ovat yh­tä­suu­ret. ok_text Oi­kein! array_claim GA[-2...g] f_nodes 20 b_nodes 11 GA[-2] = GA[g] /\ g >= -2 <=>

tai

Tau­luk­ko A in­dek­soi­daan 1:stä al­kaen, ja sii­nä on n al­kio­ta. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä pai­kas­sa 2 si­jait­se­va al­kio on mi­ni­maa­li­nen A:ssa (ts. mi­kään A:n al­kio ei ole si­tä pie­nem­pi). ok_text Oi­kein! array_claim A[1...n] f_nodes 25 b_nodes 16 n >= 2 /\ AA i; 1 <= i <= n: A[i] >= A[2] <=>

tai

Tau­luk­ko E in­dek­soi­daan 1:stä al­kaen, ja sii­nä on n al­kio­ta. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä E:n pie­nin al­kio (jo­kin niis­tä, jos on mon­ta yh­tä pien­tä) on pai­kas­sa i. ok_text Oi­kein! array_claim E[1...n] f_nodes 25 b_nodes 18 index i 1 <= i <= n /\ AA j; 1 <= j <= n: E[j] >= E[i] <=>

tai

Tau­luk­ko P in­dek­soi­daan 0:sta al­kaen, ja sii­nä on N + 1 al­kio­ta. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä P on kas­va­vas­sa jär­jes­tyk­ses­sä paik­kaan k as­ti (pai­kan k täy­tyy ol­la ole­mas­sa), ja sii­tä al­kaen vä­he­ne­väs­sä jär­jes­tyk­ses­sä. ok_text Oi­kein! array_claim P[0...N] f_nodes 39 b_nodes 35 0 <= k <= N /\ (AA i; 0 <= i < k: P[i] <= P[i+1]) /\ AA i; k <= i < N: P[i] >= P[i+1] <=>

tai

Tau­luk­ko H in­dek­soi­daan 5, …, m + 2. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä H:n pie­nin al­kio on ar­vol­taan 2. Se saat­taa esiin­tyä H:ssa useas­ti. ok_text Oi­kein! array_claim H[5...m+2] f_nodes 28 b_nodes 25 (EE i; 5 <= i <= m+2: H[i] = 2) /\ !(EE i; 5 <= i <= m+2: H[i] < 2) <=>

tai

Tau­luk­ko H in­dek­soi­daan 5, …, m + 2. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä H:n pie­nin al­kio on ar­vol­taan 2. Se ei esiin­ny H:ssa useas­ti. ok_text Oi­kein! array_claim H[5...m+2] f_nodes 32 b_nodes 31 EE i; 5 <= i <= m+2: H[i] = 2 /\ AA j; 5 <= j <= m+2 /\ j != i: H[j] > 2 <=>

tai

Tau­luk­ko H in­dek­soi­daan 4, …, l − 1. Il­man et­tä käy­tät yh­teen­las­kua tms., kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä H on kas­va­vas­sa jär­jes­tyk­ses­sä. ok_text Oi­kein! array_claim H[4...l-1] f_nodes 19 b_nodes 15 f_ban + -; AA k: AA h; 4 <= k < h < l: H[k] <= H[h] <=>

tai

Tau­luk­ko H in­dek­soi­daan 4, …, l − 1. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo et­tä H on muu­toin kas­va­vas­sa jär­jes­tyk­ses­sä, mut­ta paik­ko­jen i ja j (mis­sä i < j) al­kiot ovat vää­räs­sä jär­jes­tyk­ses­sä. ok_text Oi­kein! array_claim H[4...l-1] f_nodes 47 b_nodes 37 index i index j 4 <= i < j < l /\ H[i] > H[j] /\ AA k: AA h; 4 <= k < h < l: i = k /\ j = h \/ H[k] <= H[h] <=>

tai

Tä­mä riit­tä­köön täl­lä ker­taa!