Modified the statement of lemma TwosComplement__minTCNumber_exists. This makes its possible to prove all subsequent obligations and lemmas about  minTCNumber without requiring the (potentially inconsistent) axiom that a bit  sequence bs must be empty if "toNat bs" yields a number (i.e. is defined)  
Modified the statement of lemma TwosComplement__minTCNumber_exists.
This makes its possible to prove all subsequent obligations and lemmas about 
minTCNumber without requiring the (potentially inconsistent) axiom that a bit 
sequence bs must be empty if "toNat bs" yields a number (i.e. is defined)  

The lemma itself cannot be proven because the translation of minTCNumber lacks
the critical information that elements of the type TCNumber are nonempty. 

The lemma can be removed once the translator inserts the the proper subtype 
information. In that case we may use the (proven) lemma 
TwosComplement__minTCNumber_exists_orig. 



git-svn-id: 9ecf60ce9baff443e30a0472d3fd222fcb8117cf@9504 7b97033b-253e-4a5c-9b07-e25f9089a9fd

KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware