Proof step 528 from proof SII-loops (previous step)

Heuristic concrete calls applied rule call left

And obtained the following new goals

• Proof step 28:

  ⊦

• Proof step 527:

  〈tn0 := tn, t0 := S _ (S _ K _ K)〉 〈if m0 = 0 then abort else { TOPRED(t0; tn0): m0 -1 ; if tn0 = none ∧ ap(t0) then { RED1(t0 .1; tn0): m0 -1 ; if tn0 ≠ none then tn0 := some(tn0 .t _ t0 .2) else if value(t0 .1) then { RED1(t0 .2; tn0): m0 -1 ; if tn0 ≠ none then tn0 := some(t0 .1 _ tn0 .t) } } }〉 〈tn := tn0 ; if tn ≠ none then tn := some(tn .t _ (S _ K _ K)) else { RED1(S _ K _ K; tn): m0 ; if tn ≠ none then tn := some(S _ (S _ K _ K) _ tn .t) }〉 〈tn0 := tn ; m := m0 + 1 ; if tn0 ≠ none then tn0 := some(tn0 .t _ (S _ K _ K _ (S _ (S _ K _ K) _ (S _ K _ K)))) else { RED1(S _ K _ K _ (S _ (S _ K _ K) _ (S _ K _ K)); tn0): m ; if tn0 ≠ none then tn0 := some(S _ (S _ K _ K) _ (S _ K _ K) _ tn0 .t) }〉 〈if tn0 ≠ none then RED(tn0 .t; t2): 1 + m else t2 := S _ (S _ K _ K) _ (S _ K _ K) _ (S _ K _ K _ (S _ (S _ K _ K) _ (S _ K _ K)))〉 t2 = t, ∀ kappa0, t. kappa0 < (((((m0 + 1) + 1) + 1) + 1) + 1) + 1 → (〈RED(S _ (S _ K _ K) _ (S _ K _ K) _ (S _ (S _ K _ K) _ (S _ K _ K)); t2): kappa0 〉 t2 = t → false), m0 ≠ 0 ⊦

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]