fact: Fixpoint rhanoi3 {n : nat} := if n is n1.+1 return configuration 3 n -> configuration 3 n -> _ _ then fun c1 c2 => let p1 := c1 ldisk in let p2 := c2 ldisk in let c1' := ↓[c1] in let c2' := ↓[c2] in if p1 == p2 then [seq ↑[i]_p1 | i <- rhanoi3 c1' c2'] else let p := `p[p1, p2] in let m1 := size_rpeg c1' p + size_rpeg c2' p in let m2 := size_rpeg c1' p2 + 2 ^ n1 + size_rpeg c2' p1 in if m1 <= m2 then [seq ↑[i]_p1 | i <- rpeg c1' p] ++ [seq ↑[i]_p2 | i <- `c[p] :: lpeg p c2'] else [seq ↑[i]_p1 | i <- rpeg c1' p2] ++ [seq ↑[i]_p | i <- `c[p2] :: ppeg p2 p1] ++ [seq ↑[i]_p2 | i <- `c[p1] :: lpeg p1 c2'] else fun _ _ => [::].
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)