chiro

Lemma lemma1 : forall (st : state) (st1 st2 st3: list nat) (ins1 ins2 : list sinstr),
  s_execute st st1 ins1 = st2 ->
  s_execute st st2 ins2 = st3 ->
  s_execute st st1 (ins1 ++ ins2) = st3.
Proof.
  intros st st1 st2 st3 ins1.
  generalize dependent st1. generalize dependent st2.
  generalize dependent st3.
  induction ins1.
    intros. rewrite app_nil_l. simpl in H. subst. reflexivity.

chiro

#!/usr/bin/python

import sys, os, shutil

from os.path import *

command = "build"
dir_names = ["task", "in", "out", "sol", "etc"]

output_dir = join(abspath("./"), "atcoder", "Tasks")

chiro

contest_list <- mapM (\entity -> do
  let contest = Sq.entityVal entity
  start_time <- showTime $ contestStart contest
  end_time <- showTime $ contestEnd contest
  return $ (getContestId entity, contestName contest,
            contestJudgeType contest, start_time, end_time,
            contestSetter contest)) contests

chiro

#include <chrono>
#include <iostream>
using namespace std;

int main() {
    auto millis_since_epoch = chrono::duration_cast<chrono::milliseconds>(
        chrono::system_clock::now().time_since_epoch()).count();
    cout << millis_since_epoch << endl;
}

chiro

;; LDC 0, LDC 0, CEQ, TSEL adr 0 でadrへの無条件jmpを表現できることを使って
;; 0+..+n をループで求める
;; environment frame の破壊的変更は ST でできる
LDC 0 ; sum
LDC 10 ; n
CONS
LDF 7
AP 1
DBUG
RTN

chiro

LDC 10 ; n
LDF 5
AP 1
DBUG
RTN
LD 0 0 ; entry point
LDC 1
CGT
SEL 10 22
RTN

chiro

  /*
    List Utility Code
  */
  def arrayInit(n : Int, value : Int) : MyList[Int] = {
    if (n == 0) {
      return MyNil
    }
    return MyCons(value, arrayInit(n - 1, value))
  }

chiro

#! /usr/bin/env python
# -*- coding:utf-8 -*-

import codecs
import csv
import urllib
import urllib.request
import urllib.parse
import os
import sys

chiro

G

H

J
N個の正実数 r_1, ..., r_N (0 < r_i < 1) が与えられる。
ここからk(>=2)個選び、選んだものを x_1, ..., x_k としたとき、
必ず x_1^s + ... + x_k^s = 1 となるようなsが存在し、
選び方が 2^N - N - 1 通りあるからこのようなsは2^N-N-1個存在する。
このようなsたち全てを葉においた2分木を作ったときに、その木の"secret number"を

chiro

'((1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1)
  (1 2 2 2 2 2 2 2 2 2 1 2 2 2 2 2 2 2 2 2 1)
  (1 3 1 1 1 2 1 1 1 2 1 2 1 1 1 2 1 1 1 3 1)
  (1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1)
  (1 2 1 1 1 2 1 1 1 2 1 2 1 1 1 2 1 1 1 2 1)
  (1 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 1)
  (1 2 1 1 1 2 1 2 1 1 1 1 1 2 1 2 1 1 1 2 1)
  (1 2 1 1 1 2 1 2 2 2 1 2 2 2 1 2 1 1 1 2 1)
  (1 2 2 2 2 2 1 1 1 2 1 2 1 1 1 2 2 2 2 2 1)
  (1 1 1 1 1 2 1 0 0 0 0 0 0 0 1 2 1 1 1 1 1)