[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 7 from proof longshiftzero-zero (previous step)

⊦ bits2int (firstn (64, mklist(false, i→n(band(j, 63))) + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ')) = 0

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 8:
⊦ ¬ true ∈ bits ∧ bits ≠ [] → bits2int(bits) = 0
Proof step 9:
¬ ( ¬ true ∈ firstn (64, mklist(false, i→n(band(j, 63))) + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ') ∧ firstn (64, mklist(false, i→n(band(j, 63))) + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ') ≠ []) ⊦ bits2int (firstn (64, mklist(false, i→n(band(j, 63))) + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ')) = 0

Rule argument

seq: ⊦ ¬ true ∈ bits ∧ bits ≠ [] → bits2int(bits) = 0 subst: [bits] → [firstn (64, mklist(false, i→n(band(j, 63))) + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ')] rotate: F spec: int2bits inst: name: bits2int-zero-01

Additional information

Used terms: firstn (64, mklist(false, i→n(band(j, 63))) + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ')