[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 59 from proof exlist (conclusion)

⊦ ∃ val1, val2. flatten(val ++ val0) = val1 ++ val2

User applied rule structural induction

And obtained the following new goals

Proof step 3:
⊦ ∃ val1, val2. flatten(val ++ noval) = val1 ++ val2
Proof step 6:
⊦ ∃ val1, val2. flatten(val ++ intval(i)) = val1 ++ val2
Proof step 9:
⊦ ∃ val1, val2. flatten(val ++ byteval(by)) = val1 ++ val2
Proof step 12:
⊦ ∃ val1, val2. flatten(val ++ shortval(sho)) = val1 ++ val2
Proof step 15:
⊦ ∃ val1, val2. flatten(val ++ refval(r)) = val1 ++ val2
Proof step 18:
⊦ ∃ val1, val2. flatten(val ++ boolval(boolvar)) = val1 ++ val2
Proof step 21:
⊦ ∃ val1, val2. flatten(val ++ charval(jchar)) = val1 ++ val2
Proof step 24:
⊦ ∃ val1, val2. flatten(val ++ longval(lo)) = val1 ++ val2
Proof step 27:
⊦ ∃ val1, val2. flatten(val ++ floatval(floatvar)) = val1 ++ val2
Proof step 30:
⊦ ∃ val1, val2. flatten(val ++ doubleval(doublevar)) = val1 ++ val2
Proof step 33:
⊦ ∃ val1, val2. flatten(val ++ stringval(stringvar)) = val1 ++ val2
Proof step 40:
∀ val. ∃ val3, val2. flatten(val ++ val1) = val3 ++ val2, ∀ val. ∃ val1, val3. flatten(val ++ val2) = val1 ++ val3 ⊦ ∃ val4, val3. flatten(val ++ (val1 ++ val2)) = val4 ++ val3
Proof step 43:
⊦ ∃ val1, val2. flatten(val ++ typeval(ty)) = val1 ++ val2
Proof step 46:
⊦ ∃ val1, val2. flatten(val ++ initval(istate)) = val1 ++ val2
Proof step 49:
⊦ ∃ val1, val2. flatten(val ++ break(lbl)) = val1 ++ val2
Proof step 52:
⊦ ∃ val1, val2. flatten(val ++ continue(lbl)) = val1 ++ val2
Proof step 55:
∀ val. ∃ val3, val2. flatten(val ++ val1) = val3 ++ val2 ⊦ ∃ val3, val2. flatten(val ++ return(val1, ty)) = val3 ++ val2
Proof step 58:
⊦ ∃ val1, val2. flatten(val ++ throw(r, ty)) = val1 ++ val2

Rule argument

[VARWITHFMAVARSARG : val0, ()]

Additional information

[[CONCRETESIMPRULES : ([CSIMPGEN : javavalue generated by noval, intval, byteval, shortval, refval, boolval, charval, longval, floatval, doubleval, stringval, ++, typeval, initval, break, continue, return, throw;])]]