Theorem copy-bet-bet

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by:
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 15
• Proof steps: 30
• Used lemmas: copy-bet-up, copy-upper, arrayCopy-rec,
• Used spec theorems:
  • int-div/mod-pred-01
  • int-div/mod-pred
  • int-abs/numadd-01
  • int-div/mod-zero-05
  • int-abs/Abs-pos
• Used simplifier rules:
  • int-basic2/ls
  • int-basic1/ls-01
  • int-abs/abs-06
  • int-abs/abs-03
  • int-abs/mone-06
  • int-abs/numls-02
  • int-abs/forward-lsle
  • int-abs/forward-le
  • int-mult/two-sub-01
  • int-abs/minus-add
  • int-mult/numeq-03
  • int-div/mod-same
  • int-mult/dist-rmerge
  • int-mult/succ-rmerge
  • int-mult/eq-pos
  • int-basic1/forward-pos
  • int-abs/sub-add-04
  • int-abs/succ-01
  • int-mult/associativity
  • int-mult/one
  • int-mult/numle-04
  • int-abs/sub-sub-04
  • int-mult/commutativity
  • int-abs/lels-02
  • oelem/intlista/transitivity
  • int-mult/add-mult-two
  • refkey/inj-01
  • oelem/intlista/lel
  • int-basic2/add-in
  • int-abs/numsub
  • storekey/inj-04
  • refkey/inj
  • int-abs/sub-sub
  • intnat/abs-pred
  • int-abs/lels
  • int-abs/lels-03
  • oelem/intlista/sls
  • int-abs/sub-ls-01
  • int-abs/lels-04
  • int-abs/les
  • javastore/lookup-if
  • int-abs/sub-add-01
  • int-abs/sub-le
  • int-abs/lels-01
  • int-div/mod-zero-04
  • int-abs/sub-eq
  • int-basic2/ax-04
  • int-abs/sub-ls
  • int-basic2/ls-01
  • int-abs/succ-02
  • int-abs/ler
  • int-abs/sub-le-01
  • int-abs/lep-02
  • int-abs/leone
  • oelem/intlista/irreflexivity
  • int-abs/sub-sub-03
  • int-abs/sub-add-06
  • int-abs/Sub-def
  • int-abs/forward-le-05
  • int-basic2/add-a
  • int-basic2/ls-02
  • int-basic2/add-c
  • int-abs/forward-lels