Theorem maxinf-inf

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

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 4
• Proof steps: 11
• Used lemmas: maxinf-def,
• Used spec theorems:
  • Used simplifier rules:
    • nat-inf-basic/elim
    • nat-inf/less-fin
    • nat-inf-basic/disj
    • nat-basic1/f