how do i do this in isabelle?
(* how do i do this?? *) | |
function simplex_count :: "int⇒int⇒int" where | |
"simplex_count 0 0 = 1" | | |
"simplex_count 0 1 = 0" | | |
"simplex_count 1 0 = 2" | | |
"simplex_count n k = (simplex_count (n-1) k + simplex_count n (k-1))" | |
sorry | |
lemma simplex_count_lemma: | |
assumes "n simplex S" fixes k assumes "0 ≤ k" and "k ≤ n" | |
shows "k d_face_count S = simplex_count n k" | |
sorry |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment