Theorem mod-rec-any

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: mod-mult-add, mod-plus,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 5
• Proof steps: 10
• Used lemmas: mod-mult-04, mod-zero-neg, mod-rec-neg, mod-zero, mod-rec,
• Used spec theorems:
  • int-abs/Abs-neg
• Used simplifier rules:
  • int-abs/forward-le-05
  • int-abs/forward-le-02
  • oelem/intlista/transitivity
  • int-abs/lels-01
  • int-abs/neg-03
  • int-abs/zero-gels-01
  • int-abs/forward-le-01
  • int-abs/Sub-def
  • int-abs/sub-eq
  • int-abs/abs-06
  • int-abs/forward-lsle
  • int-abs/forward-le
  • int-abs/lels
  • int-abs/sub-ls
  • int-basic2/add-zero
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/neg-06
  • int-abs/minus-sub
  • int-abs/sub-ls-01
  • int-mult/add-mult-two
  • int-abs/sub-le-01
  • int-abs/lep-01
  • int-abs/anti
  • oelem/intlista/lel
  • int-abs/Abs-pos
  • int-basic2/ls
  • int-basic1/ls-01