This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; Ubuntuでの設定です。.emacs.dの中身とかは察して下さい | |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | |
;; Set-up modes ;; | |
(show-paren-mode t) | |
(define-key global-map [f4] 'kill-frame) | |
(define-key global-map [f5] 'make-frame) | |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | |
;; Program modes ;; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import ssreflect ssrbool ssrnat. | |
Definition nand_b (b0 : bool) (b1 : bool) : bool := | |
match b0 with | |
| true => (~~ b1) | |
| false => true | |
end. | |
Lemma nand_lemma : forall (b0 b1 : bool), (nand_b b0 b1) = (~~(b0 && b1)). | |
Proof. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import ssreflect ssrbool ssrnat. | |
(* Software Foundation 練習問題: ★★, recommended (basic_induction) *) | |
Lemma ゼロを掛けるとゼロになる : forall (n:nat), n*0 = 0. | |
Proof. | |
move=> n. | |
induction n as [| m]. | |
trivial. (* 0*0 == 0 *) | |
rewrite mulSnr. (* m.+1 * 0 ~~~> m * 0 + 0 *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import ssreflect ssrbool. | |
Axiom SET : Type. | |
Axiom membership : SET -> SET -> Prop. | |
Notation "x ∈ y" := (membership x y) (at level 100) : type_scope. | |
Axiom Extensionality : forall (x y: SET), (forall (z : SET), ((z ∈ x) <-> (z ∈ y))) <-> (x = y). | |
Axiom emptyset : SET. | |
Axiom EmptySetAxiom : (forall (z: SET), ~(z ∈ emptyset)). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(*--- Kuratowski's Definition of ordered-pairs ---*) | |
Definition ordered_pair (x y : SET) : SET := | |
{ {{x}} , { x , y } }. | |
Notation "\( x , y \)" := (ordered_pair x y) (at level 35). | |
Lemma 補題_Singletonのequality : forall (x y z : SET), {{x}} = {y, z} -> x = y. | |
Proof. | |
move=> y x z; move. | |
case=> Hsingleton. | |
assert ( x ∈ {x, z} ) as Hxinx. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import ssreflect. | |
Axiom SET : Type. | |
Definition Var := nat. | |
Definition Term := nat. | |
(* | |
Definition equalS : nat := 0. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/bin/sh | |
#export WORKDIR=/cygdrive/c/Users/tmiy/Desktop | |
#export RE="<a href=\".*\"" | |
#export FILTERED=./testdata.txt | |
## main ## | |
cd /cygdrive/c/Users/tmiy/Desktop/Apple_files ## | |
grep -irho "<a href=\".*\"" ./ > ../testdata.txt ## | |
sed -e "s/\"//g" ../testdata.txt | sed -e "s/<A HREF=//g" > ../testdata2.txt ## | |
##cat ../testdata.txt ## | |
##cat ../testdata2.txt ## |