Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/trace_simp_output

Created July 13, 2018 07:11
Show Gist options
  • Save kbuzzard/1a01ad2bc29aad1c257452c4d2d894d5 to your computer and use it in GitHub Desktop.
Save kbuzzard/1a01ad2bc29aad1c257452c4d2d894d5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
trace_simp_output
0. [simplify.rewrite] [multiset.mem_singleton]: a ∈ c :: 0 ==> a = c
0. [simplify.rewrite] [ne.def]: c ≠ a ==> ¬c = a
0. [simplify.rewrite] [sub_eq_add_neg]: 2 - ↑(HC (erase C2 a) _ L2) ==> 2 + -↑(HC (erase C2 a) _ L2)
0. [simplify.rewrite] [sub_eq_add_neg]: 4 - ↑(HL (erase L2 a) _) ==> 4 + -↑(HL (erase L2 a) _)
0. [simplify.rewrite] [sub_eq_add_neg]: 2 -
↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ) (L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2 _ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _)))
0) ==> 2 +
-↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ) (L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2 _ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _)))
0)
0. [simplify.rewrite] [multiset.pmap_cons]: pmap
(λ (a : ℕ) (h : a ∈ c :: 0),
a - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
0)))
(c :: 0)
_ ==> (c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on (erase (c :: 0) c)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
0))) ::
pmap
(λ (a : ℕ) (h : a ∈ c :: 0),
a - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _)))
L2
_)))
0)))
0
_
0. [simplify.rewrite] [multiset.mem_singleton]: c ∈ c :: 0 ==> c = c
0. [simplify.rewrite] [eq_self_iff_true]: c = c ==> true
0. [simplify.rewrite] [not_true]: ¬true ==> false
0. [simplify.rewrite] [ne.def]: c ≠ c ==> ¬c = c
0. [simplify.rewrite] [eq_self_iff_true]: c = c ==> true
0. [simplify.rewrite] [not_true]: ¬true ==> false
0. [simplify.rewrite] [multiset.erase_cons_head]: erase (c :: 0) c ==> 0
0. [simplify.rewrite] [multiset.mem_singleton]: a ∈ c :: 0 ==> a = c
0. [simplify.rewrite] [ne.def]: c ≠ a ==> ¬c = a
0. [simplify.rewrite] [multiset.pmap_zero]: pmap
(λ (a : ℕ) (h : a ∈ c :: 0),
a - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
0)))
0
_ ==> 0
0. [simplify.rewrite] [multiset.mem_singleton]: a ∈ c :: 0 ==> a = c
0. [simplify.rewrite] [ne.def]: c ≠ a ==> ¬c = a
0. [simplify.rewrite] [sub_eq_add_neg]: 2 -
↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ) (L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2 _ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _)))
L2) ==> 2 +
-↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ) (L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2 _ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _)))
L2)
0. [simplify.rewrite] [multiset.pmap_cons]: pmap
(λ (a : ℕ) (h : a ∈ c :: 0),
a - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
L2)))
(c :: 0)
_ ==> (c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on (erase (c :: 0) c)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
L2))) ::
pmap
(λ (a : ℕ) (h : a ∈ c :: 0),
a - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _)))
L2
_)))
L2)))
0
_
0. [simplify.rewrite] [multiset.mem_singleton]: a ∈ c :: 0 ==> a = c
0. [simplify.rewrite] [ne.def]: c ≠ a ==> ¬c = a
0. [simplify.rewrite] [multiset.pmap_zero]: pmap
(λ (a : ℕ) (h : a ∈ c :: 0),
a - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on (erase (c :: 0) a)
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
L2)))
0
_ ==> 0
0. [simplify.rewrite] [sub_eq_add_neg]: 4 - ↑(HL (erase L2 a) _) ==> 4 + -↑(HL (erase L2 a) _)
0. [simplify.rewrite] [multiset.cons_add]: (c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
L2))) ::
0 +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _ ==> (c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
L2))) ::
(0 + pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _)
0. [simplify.rewrite] [zero_add]: 0 + pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _ ==> pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _
0. [simplify.rewrite] [sub_eq_add_neg]: 4 -
↑(strong_induction_on (erase 0 a)
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
((c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap
(λ (a : ℕ) (h : a ∈ C2),
a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap
(λ (a : ℕ) (h : a ∈ L2),
a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _)))
L2
_)))
L2))) ::
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _))) ==> 4 +
-↑(strong_induction_on (erase 0 a)
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
((c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap
(λ (a : ℕ) (h : a ∈ C2),
a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap
(λ (a : ℕ) (h : a ∈ L2),
a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _)))
L2
_)))
L2))) ::
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _)))
0. [simplify.rewrite] [multiset.pmap_zero]: pmap
(λ (a : ℕ) (h : a ∈ 0),
a - 4 +
int.nat_abs
(4 +
-↑(strong_induction_on (erase 0 a)
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
((c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ)
(HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap
(λ (a : ℕ) (h : a ∈ C2),
a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap
(λ (a : ℕ) (h : a ∈ L2),
a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _)))
L2
_)))
L2))) ::
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))))
0
_ ==> 0
0. [simplify.rewrite] [multiset.cons_add]: (c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
0))) ::
0 +
0 ==> (c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
_)))
0))) ::
(0 + 0)
0. [simplify.rewrite] [add_zero]: 0 + 0 ==> 0
0. [simplify.rewrite] [N_min_singleton]: N_min
((c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
(L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2)))
C2
_ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _)))
L2
_)))
0))) ::
0) ==> c - 2 +
int.nat_abs
(2 +
-↑(strong_induction_on 0
(λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ) (L : multiset ℕ),
strong_induction_on L
(λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
N_min
(pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2 _ +
pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2 _)))
0))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment