Re: [Rodin-b-sharp-user] Total functions and the empty set

[<kim...@ko...>]

Hello,

No induction is needed. One simple interactive proof proceeds as follows:
1) Contradict the goal.
2) Apply "remove negation in hypothesis" until there is no negation.
3) Apply "remove inclusion in hypothesis".
4) Apply "instantiate universally quantified variables" using (0 .. n) × {0} as the value of the only present universally quantified variable.

With best regards,
Kimmo Varpaaniemi

"Jonathan S. Ostroff" [jon...@yo...] kirjoitti: 
> (*) Given n>0 I would like to prove that: ¬ (0%n ’ {0} † )
> 
> [More generally I would like to prove that (**) ¬ (0%n ’ {0} = ), but the above theorem is the critical one. This is the PO for initializing all values in an array to zero.]
> 
> I would have thought that (*) and (**) would be discharged automatically as part of the background theory. This does not happen and I can see no way of guiding the proof, other than by induction on n).
> 
> I have not done an inductive proof before:
> 
> http://wiki.event-b.org/index.php/Induction_proof
> 
> Am I doing this correctly? One introduces the "proof key" �s" s†1 '1s'(�n"nsÒn+1s)Ò1†s as an axiom in a context (this generates a warning because n is already used), and then instantiate the proof key appropriately. I tried this and after a long proof tree everything eventually discharges (I can forward my proof if needed).
> 
> This seems like quite a bit of work to prove (*).
> 
> Your advice would be much appreciated, as usual.
> 
> Thanks
> 
> Jonathan
> 
> 
> 
> 
> 
> 
> ------------------------------------------------------------------------------
> Download Intel® Parallel Studio Eval
> Try the new software tools for yourself. Speed compiling, find bugs
> proactively, and fine-tune applications for parallel performance.
> See why Intel Parallel Studio got high marks during beta.
> http://p.sf.net/sfu/intel-sw-dev
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
>