sunaemon

#!/usr/bin/python
import re
import sys

reg1 = re.compile(r'\[\[File:([^,]*?),.*?%\]\]')
reg11 = re.compile(r'\[\[File:([^,]*?),left\]\]')
reg12 = re.compile(r'\[\[File:([^,]*?),right\]\]')
reg2 = re.compile(r'\[\[File:([^\]]*)_[^\]]+\.\./([^\]]*)\]\]')
reg3 = re.compile(r'\[\[File:([^\/]*)_(.*?)/(.*?)\]\]')
reg4 = re.compile(r'<del>(.*?)</del>')

sunaemon

$ aptitude install firmware-iwlwifi

sunaemon

Definition tautology : forall P : Prop, P -> P
  := fun x => (fun x => x).

Definition Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P
  := fun P Q H HH => proj1 H (proj2 H HH).


Definition Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q
  := fun P Q H HH => match H with

sunaemon

Require Import Arith.

Definition Nat : Type :=
  forall A : Type, (A -> A) -> (A -> A).

Print Nat.

Definition NatPlus(n m : Nat) : Nat :=
 fun A f x => n A f (m A f x).

sunaemon

Parameter A : Set.
 
Definition Eq := fun a b:A => forall ee : A->A->Prop, ee a a -> ee a b.
 
Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
intros x y.
unfold Eq.
split.
+ intro H.

sunaemon

Theorem hoge : forall P Q R : Prop, P \/ ~(Q \/ R) -> (P \/ ~Q) /\ (P \/ ~R).
Proof.
  refine (fun P Q R H => _).
  refine (match H with
              | or_introl HP => _
              | or_intror  HnQR => _
          end).
  - exact (conj (or_introl HP) (or_introl HP)).
  - refine (conj _ _).
    + refine (or_intror (fun HQ => _)).

sunaemon

Lemma ABC_iff_iff :
    forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
Require Import Classical. 
intros; tauto.
Qed.

Goal
  forall P Q R : Prop,

sunaemon

FROM debian:wheezy

MAINTAINER sunaemon <@sunaemon0>

# install packages
RUN echo 'Acquire::http { Proxy "http://hogehoge:3142"; }; ' > /etc/apt/apt.conf.d/50-apt-cacker.conf
ENV DEBIAN_FRONTEND noninteractive
RUN apt-get update && apt-get upgrade -y

#install tools for logging and process administration

sunaemon

#include <sys/select.h>
#include <fcntl.h>
#include <stdio.h>
int main()
{
    int sock = open("/dev/urandom", O_RDONLY);
    int r;
    fd_set rfds;
    FD_ZERO(&rfds);
    FD_SET(sock, &rfds);

sunaemon

FROM debian:wheezy

# install packages
ENV DEBIAN_FRONTEND noninteractive
RUN apt-get update && apt-get upgrade -y

#install tools for logging and process administration
RUN apt-get install -y monit rsyslog
WORKDIR /
RUN apt-get install -y ruby ruby-dev build-essential wget