Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/function

Created August 5, 2016 00:23
Show Gist options
  • Save mukeshtiwari/20754038ae429a24f4f4512bc3f902ee to your computer and use it in GitHub Desktop.
Save mukeshtiwari/20754038ae429a24f4f4512bc3f902ee to your computer and use it in GitHub Desktop.
Download ZIP
Raw
function
k : nat
u, v : cand
l : list (cand * cand)
H1 : fold_left
(fun (x : bool) (b : cand) => x && (bool_in (b, snd (u, v)) l || el k (fst (u, v), b)))
cand_all true = true
b : cand
============================
In (b, snd (u, v)) l \/ edge (fst (u, v)) b <= k
@mukeshtiwari
Copy link
Author

forall (k : nat) (p : cand * cand) (l : list (cand * cand)),
fold_left (fun (x : bool) (b : cand) => x && (bool_in (b, snd p) l || el k (fst p, b)))
cand_all true = true -> forall b : cand, In (b, snd p) l / edge (fst p) b <= k

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment