Theorem s2n-app

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: n2s-s2n-identity, s2n-rec-last,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 2
• Proof steps: 8
• Used lemmas: s2n-rec-01,
• Used spec theorems:
  • nat-mult/dist
• Used simplifier rules:
  • string-append/append-base
  • string-append/rest-one
  • nat-mult/one
  • string-less/Length-empty
  • string-append/first-one
  • string-append/empty-01
  • string-append/first-01
  • nat-pot/add
  • nat-basic2/pred
  • string-append/rest-01
  • string-less/len-zero
  • nat-basic2/z-01
  • nat-basic2/one-03
  • nat-basic2/oz
  • nat-basic1/one
  • string-less/len-app
  • string-less/Length-rec
  • string-data/elim
  • string-append/assoc
  • string-append/one
  • string-append/chartostring-01
  • nat-basic2/c
  • nat-basic2/a
  • nat-basic2/eq-01
  • nat-mult/mult-c
  • nat-mult/mult-a