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

Heuristic weak unfold applied rule call left

And obtained the following new goals

• Proof step 265:

  ⊦

• Proof step 270:

  〈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 tn1 := 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 tn1 := some(v1 _ v3 _ (v2 _ v3)) else tn1 := none else tn1 := none〉 tn1 = tn0, ∀ n0, t, tn1, tn0. n0 < m + 1 → (〈RED1(t; tn3): n0 〉 tn3 = tn1 ∧ 〈RED1(t; tn3)〉 tn3 = tn0 ∧ tn0 ≠ tn1 → false), tn0 ≠ some(t4 _ t1 _ (t3 _ t1)), m ≠ 0, tn0 ≠ none, value(t4), value(t3), value(t1) ⊦

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]