Proof step 237 from proof kappa-RED1 (previous step)

Heuristic weak unfold applied rule call left

And obtained the following new goals

• Proof step 231:

  ⊦

• Proof step 236:

  〈if ap(S _ t4 _ t3 _ t1) ∧ ap((S _ t4 _ t3 _ t1) .1) ∧ (S _ t4 _ t3 _ t1) .1 .1 = K ∧ value((S _ t4 _ t3 _ t1) .1 .2) ∧ value((S _ t4 _ t3 _ t1) .2) then tn0 := some((S _ t4 _ t3 _ t1) .1 .2) else if ap(S _ t4 _ t3 _ t1) ∧ ap((S _ t4 _ t3 _ t1) .1) ∧ ap((S _ t4 _ t3 _ t1) .1 .1) ∧ (S _ t4 _ t3 _ t1) .1 .1 .1 = S then let v1 = (S _ t4 _ t3 _ t1) .1 .1 .2, v2 = (S _ t4 _ t3 _ t1) .1 .2, v3 = (S _ t4 _ t3 _ t1) .2 in if value(v1) ∧ value(v2) ∧ value(v3) then tn0 := some(v1 _ v3 _ (v2 _ v3)) else tn0 := none else tn0 := none〉 tn0 = none, 〈RED1(t1; tn4)〉 tn4 = some(t0), 〈RED1(S _ t4 _ t3; tn2)〉 tn2 = none, ∀ n0, t, tn1, tn0. n0 < m + 1 → (〈RED1(t; tn3): n0 〉 tn3 = tn1 ∧ 〈RED1(t; tn3)〉 tn3 = tn0 ∧ tn0 ≠ tn1 → false), m ≠ 0, S _ t4 _ t3 _ t0 ≠ t4 _ t1 _ (t3 _ t1), value(t4), value(t3), value(t1), value(S _ t4 _ t3) ⊦

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]