[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
,
Proof step 9 from proof append-eqlen-01 (
previous step
)
str3 + str0 = str4 + str2, # str0 = # str2, ∀ str0, str2, str1. # str0 = # str2 ∧ str3 + str0 = str1 + str2 → str3 = str1 ∧ str0 = str2 ⊦ char0 ' + str4 = "", str3 = str4 ∧ str0 = str2
User applied rule all left
And closed the goal!
Rule argument
pos: left 3 terms: str0, str2, str4 abort: F discard: T computed: T
Additional information
Used terms: str0, str2, str4