Proof step 35 from proof kappa-TOPRED (previous step)

Heuristic weak unfold applied rule call left

And obtained the following new goals

• Proof step 28:

  ⊦

• Proof step 34:

  〈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 tn := 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 tn := some(v1 _ v3 _ (v2 _ v3)) else tn := none else tn := none〉 tn = tn0, tn0 ≠ none, n ≠ 0, ¬ (value(t4) ∧ value(t3) ∧ value(t1)) ⊦

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]