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