[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 1 from proof fun-reduces-imp-app-reduces (
previous step
)
⊦ t => t' ↔ (∃ C. (∃ v1, v2. t = C[K _ v1 _ v2] ∧ t' = C[v1] ∧ value(v1) ∧ value(v2) ∧ context(C)) ∨ (∃ v1, v2, v3. t = C[S _ v1 _ v2 _ v3] ∧ t' = C[v1 _ v3 _ (v2 _ v3)] ∧ value(v1) ∧ value(v2) ∧ value(v3) ∧ context(C)))
Lemma
one-step-red-def