kmill

/-
A constructive proof of the cantor diagonalization argument: there is
no bijection between a set and its powerset.  Since Lean is based on
type theory, we use a type α rather than a set, and for convenience we
use (α → bool) to represent the powerset, i.e. indicator functions on α.
-/

import data.equiv.basic

open function

kmill

inductive binary_tree : Type
| root : binary_tree
| tree : binary_tree → binary_tree → binary_tree

namespace binary_tree

def mirror : binary_tree → binary_tree
| root := root
| (tree a b) := tree (mirror b) (mirror a)

kmill

This is an analysis of https://codegolf.stackexchange.com/a/203685/78112
like in https://gist.github.com/kmill/266ef6bb5690f9c26110673dcc59f710

Input: n A

1. M1    +      A -> M2 + 10 B
2  M1             -> M2 + A
3. M2  +  A + Div -> M1 + B
4. M2 + 4 B + Div -> M1 + A
5. M2             -> Count

kmill

See https://codegolf.stackexchange.com/a/203682/78112

This is a description of Anders Kaseorg's solution to the code golf problem of making a program in FRACTRAN
that detects whether or not the Collatz sequence starting from the given number eventually reaches 1.

FRACTRAN programs can be thought of as being a list of chemical reactions with no catalysts (chemical
species that appear as both reagents and products).  Given a fraction c/d, the prime factors present
in d (with multiplicity) are the reagent species, and the prime factors present in c (with
multiplicity) are the product species.  Since fractions are reduced, a species is only ever either a
reagent or a product in a given reaction.

kmill

<?php
$parts = explode("\n", $_POST['msg'], 2);
$msg = $parts[0];
if (strlen($msg) > 0) {
  $f = fopen("messages.txt", "a") or die("Unable to open file");
  fwrite($f, $msg . "\n");
  fclose($f);
}
echo "Success";

kmill

^Did you know that (the (fall|spring) equinox|the (winter|summer) (solstice|Olympics)|the (earliest|latest) (sunrise|sunset)|daylight savings? time|leap (day|year)|Easter|the (harvest|super|blood) moon|Toyota truck month|shark week) (happens (earlier|later|at the wrong time) every year|drifts out of sync with the (sun|moon|zodiac|(Gregorian|Mayan|lunar|iPhone) calendar|atomic clock in Colorado)|might (not happen|happen twice) this year) because of (time zone legislation in (Indiana|Arizona|Russia)|a decree by the pope in the 1500s|(precession|libration|nutation|libation|eccentricity|obliquity) of the (moon|sun|Earth's axis|equator|prime meridian|(international date|Mason-Dixon) line)|magnetic field reversal|an arbitray decision by (Benjamin Franklin|Isaac Newton|FDR))\? Apparently (it causes a predictable increase in car accidents|that's why we have leap seconds|scientists are really worried|it was even more extreme during the (bronze age|ice age|Cretaceous|1990s)|there's a proposal to fix it, but it (will ne

kmill

# Example of Todd-Coxeter to compute S_3 from relations

idents = []
neighbors = []
to_visit = 0

ngens = 2
def op_dir(d):
    return d+1-2*(d%2)

kmill

# Example of Todd-Coxeter to compute S_3 from relations

idents = []
neighbors = []
to_visit = []
visited = set()

op_dir = [1, 0, 3, 2]

def find(c):

kmill

num = 1
while True:
    rems = (num % 3, num % 4, num % 5, num % 6)
    print num, rems
    if rems == (1, 2, 3, 4):
        print num
        break
    num += 1

kmill

num = 1
while True:
    if num % 3 == 1 and num % 4 == 2 and num % 5 == 3 and num % 6 == 4:
        print num
        break
    num += 1