fact: Fixpoint lhanoi3 {n : nat} : configuration 3 n -> configuration _ n -> _ := match n with | 0 => fun _ _ => [::] : seq (configuration _ 0) | _.+1 => fun c1 c2 => let p1 := c1 ldisk in let p2 := c2 ldisk in if p1 == p2 then [seq ↑[i]_p2 | i <- lhanoi3 ↓[c1] ↓[c2]] else let p3 := `p[p1, p2] in if lrel p1 p2 then [seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p3]] ++ [seq ↑[i]_p2 | i <- `c[p3] :: lhanoi3 `c[p3] ↓[c2]] else [seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p2]] ++ [seq ↑[i]_p3 | i <- `c[p2] :: lhanoi3 `c[p2] `c[p1]] ++ [seq ↑[i]_p2 | i <- `c[p1] :: lhanoi3 `c[p1] ↓[c2]] end.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)