Skip to content

Instantly share code, notes, and snippets.

View qnighy's full-sized avatar

Masaki Hara qnighy

View GitHub Profile
@qnighy
qnighy / LJ.v
Created December 22, 2012 12:57 — forked from anonymous/LJ.v
View LJ.v
Require Import Coq.Lists.List.
Require Import Coq.Sorting.Permutation.
Require Import Coq.Relations.Relations.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Arith.Arith.
Require Import MyPermutations.
Inductive PProp:Set :=
| PPbot : PProp
View result
(1*(2/(3/((4-(5-(6*(7*8))))*9))))
(1*(2/(3/((4-(5-((6*7)*8)))*9))))
(1+(2+(3*((4*((5+6)*(7+8)))+9))))
(1*(2*(3*((4*((5*6)+(7*8)))-9))))
(1*(2/(3/(((4+5)*(6*(7*8)))-9))))
(1*(2/(3/(((4+5)*((6*7)*8))-9))))
(1*(2/(3/(((4-5)+(6*(7*8)))*9))))
(1*(2/(3/(((4-5)+((6*7)*8))*9))))
(1+(2+(3*(((4*(5+6))*(7+8))+9))))
(1*(2/(3/((((4+5)*6)*(7*8))-9))))