[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem dist-rsplit
⊦ i * (j + j0) = i * j + i * j0
Type: A user defined theorem
Validity: The proof is valid.
Features: dist-split,
Comment:
Used by:
associativity
,
eq-dist
,
eq-succ
,
ls-pos
,
modeqp
,
modlsp
,
modzero-01
,
modzero-02
,
modzero-03
,
modzero-04
,
modzero-05
,
modzero-06
,
zero-ge-add
,
Used by units in proved state:
int-pot
,
int-gcd
,
int-div
,
int-square
,
int-min
,
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 4
Proof steps: 9
Used lemmas:
succ-rsplit
,
Mult-zero
,
Used spec theorems:
Used simplifier rules:
int-basic2
/
add-zero
int-basic2
/
add-pred
int-basic1
/
elim-pred
int-basic2
/
pred
int-basic2
/
succ-01
int-basic2
/
add-in
int-basic2
/
add-a
int-basic2
/
add-c