Theorem stutf-nonempty

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: localsimp, simp,
• Comment:
• Used by: inv-get-inverse, inv-get-inverse-between, inv-get-inverse-last, inv-get-lslen, inv-inverts-leq, leninv-inf, leninv-succ, leninv-zero, lsleninv-1, stutf-alltakenmax,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 1
• Used lemmas: not-stutf-empty,
• Used spec theorems:
  • Used simplifier rules: