fetburner

let merge_sort ( <= ) =
  (* 非減少列をマージして減少列を得る *)
  let rec rev_merge l1 l2 acc =
    match l1, l2 with
    | [], l2 -> List.rev_append l2 acc
    | l1, [] -> List.rev_append l1 acc
    | h1 :: t1, h2 :: t2 ->
        if h1 <= h2
        then rev_merge t1 l2 (h1 :: acc)
        else rev_merge l1 t2 (h2 :: acc)

fetburner

(* 非減少列をマージして減少列を得る *)
let rec rev_merge ( <= ) l1 l2 acc =
  match l1, l2 with
  | [], l2 -> List.rev_append l2 acc
  | l1, [] -> List.rev_append l1 acc
  | h1 :: t1, h2 :: t2 ->
      if h1 <= h2
      then rev_merge ( <= ) t1 l2 (h1 :: acc)
      else rev_merge ( <= ) l1 t2 (h2 :: acc)

fetburner

local
  fun revMerge' op<= [] ys acc = List.revAppend (ys, acc)
    | revMerge' op<= xs [] acc = List.revAppend (xs, acc)
    | revMerge' op<= (x :: xs) (y :: ys) acc =
        if x <= y then revMerge' op<= xs (y :: ys) (x :: acc)
        else revMerge' op<= (x :: xs) ys (y :: acc)

  fun sort' op<= op> 2 (x :: y :: _) =
        if x <= y then [x, y] else [y, x]
    | sort' op<= op> 3 (x :: y :: z :: _) =

fetburner

{-# LANGUAGE Strict #-}
{-# LANGUAGE StrictData #-}

main :: IO ()
main = do
  s <- getLine
  let
    n = read s
    (_, x, y) = go 1 $ max 0 $ ceiling $
      logBase 2 (fromIntegral n) - 1.55849716603186539

fetburner

Require Import Ensembles.

Section KnasterTarski.
  Variable U : Type.
  Variable f : Ensemble U -> Ensemble U.
  Hypotheses monotone : forall X Y, Included _ X Y -> Included _ (f X) (f Y).

  Definition lfp : Ensemble U := fun x => forall X, Included _ (f X) X -> X x.

  Lemma lfp_lower_bound X : Included U (f X) X -> Included _ lfp X.

fetburner

Require Import Bool Arith Omega.

Variable var : Set.
Hypotheses var_eq_dec : forall x y : var, { x = y } + { x <> y }.

Definition state := var -> nat.

Definition update {A} x n (s : var -> A) := fun y =>
  if var_eq_dec x y then n else s y.

fetburner

Require Import List Omega Program.

Section ListPairDP.
  Variable A : Set.
  Variable X : Set.
  Variable f_nil_nil : A.
  Variable f_nil_l2s : list (A * X).
  Variable f_l1_nils : list (A * X).
  Variable f_cons_cons : X -> X -> A -> A -> A -> A.
  Variable R : list X -> list X -> A -> Prop.

fetburner

let rec fold_tournament dir f = function
  | [x] -> x
  | xs ->
      List.fold_left (fun (acc, prev) x ->
        match prev with
        | None -> (acc, Some x)
        | Some y -> ((if dir then f y x else f x y) :: acc, None)) ([], None) xs
      |> (function
          | (acc, None) -> acc
          | (acc, Some x) -> x :: acc)

fetburner

#include <stdio.h>
#include <stdlib.h>
#include <memory.h>

/*
 * merge(a, n, b, m, c)
 * 昇順にソートされた長さnの配列aと昇順にソートされた長さmの配列bを受け取り，
 * マージした結果を配列cに破壊的代入する
 * 配列cはn+m個の要素を格納できる必要がある
 * 配列cのアドレスと配列aのアドレス，配列cのアドレスと配列bのアドレスは重なりを持たない必要がある

fetburner

(*
 * dp f_nil_nil f_nil_l2s f_l1_nils f_cons_cons l1 l2
 * 漸化式
 * f [] [] = f_nil_nil
 * f [] (drop i l2) = nth f_nil_l2s i
 * f (drop i l1) [] = nth f_l1_nils i
 * f (x :: l1) (y :: l2) = f_cons_cons x y (f l1 l2) (f (x :: l1) l2) (f l1 (y :: l2))
 * を満たすような f について，dpで f l1 l2 を求める
 * ただし，事前条件 |f_l1_nils| = |l1| かつ |f_nil_l2s| = |l2| を満たす必要がある
 * f_cons_cons x y dp_l1'_l2' dp_l1_l2' dp_l1'_l2 が時間計算量，空間計算量共にO(1)の場合，