Library hydras.Hydra.KP_example
Pierre Casteran, Univ. Bordeaux and LaBRI
The hydra from page 286 of KP
initial state
Definition h0 : Hydra :=
hyd2 (hyd2 (hyd_mult head 3)
(hyd1 (hyd1 head)))
(hyd2 head
(hyd2 head head)).
Fact F1 : hsize h0 = 14.
Fact F2 : height h0 = 4.
after stage 1
Definition h1 :=
hyd2 (hyd3 (hyd_mult head 2)
(hyd_mult head 2)
(hyd1 (hyd1 head)))
(hyd2 head
(hyd2 head head)).
After stage 2
Notation hyd4 h1 h2 h3 h4 :=
(node (hcons h1 (hcons h2 (hcons h3 (hcons h4 hnil))))).
Let h' := hyd1 (hyd_mult head 2).
Definition h2 :=
hyd4 (hyd3 (hyd_mult head 2)
(hyd_mult head 2)
(hyd1 (hyd1 head)))
h' h' h'.
After stage 3
Definition h3 := hyd4
(node (hcons_mult (hyd1 head) 4
(hcons (hyd2 head head)
(hcons (hyd1 (hyd1 head))
hnil))))
h' h' h'.
Fact h0_h1 : round_n 1 h0 h1.
Fact h1_h2 : round_n 2 h1 h2.
Fact h2_h3 : round_n 3 h2 h3.
Lemma battle_example : rounds standard 1 h0 4 h3.
= 28