daily pastebin goal
3%
SHARE
TWEET

Untitled

a guest Mar 13th, 2018 48 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. lemma all_exist:
  2. fixes a b :: nat and c :: int*
  3. assumes "..."*
  4. shows "<exists> a1 a2 a3 a4 a5 a6 a7 :: int. {around 15 equations and inequalities that define the integers}*
  5. proof -
  6.     ...
  7.     from s1 s2 ... sn have final: "<exists> a1 a2 a3 a4 a5 a6 a7 :: int. {all those 15 equations and inequalities that define a1 to a7}" by force
  8.     from final show ?thesis sorry
  9. qed
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top