daily pastebin goal
43%
SHARE
TWEET

Untitled

a guest Mar 13th, 2018 48 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  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