Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/false_in_context.v

Created September 15, 2016 04:40
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mukeshtiwari/01af63d4ac779af6766a9d656bcee47c to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mukeshtiwari/01af63d4ac779af6766a9d656bcee47c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
false_in_context.v
A : Type
k : nat
O : (A -> bool) -> A -> bool
Hmon : mon O
l : list A
Hin : forall a : A, In a l
Hlen : length l <= k
n : nat
Hlel : k < n
R : length (filter (iter O (k + 1) full_ss) l) + (k + 1) <= length l
============================
pred_subset (iter O k full_ss) (iter O n full_ss)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment