Proof step 74 from proof reduction-is-topred-in-ctxt (conclusion)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ⊦ K => t' ↔ (∃ C, t0, t1. context(C) ∧ K = C[t0] ∧ t0 =>top t1 ∧ t' = C[t1])

• Proof step 6:

  ⊦ S => t' ↔ (∃ C, t0, t1. context(C) ∧ S = C[t0] ∧ t0 =>top t1 ∧ t' = C[t1])

• Proof step 73:

  ∀ t'. t0 => t' ↔ (∃ C, t2, t1. context(C) ∧ t0 = C[t2] ∧ t2 =>top t1 ∧ t' = C[t1]), ∀ t'. t1 => t' ↔ (∃ C, t0, t2. context(C) ∧ t1 = C[t0] ∧ t0 =>top t2 ∧ t' = C[t2]) ⊦ t0 _ t1 => t' ↔ (∃ C, t2, t3. context(C) ∧ t0 _ t1 = C[t2] ∧ t2 =>top t3 ∧ t' = C[t3])

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPGEN : term generated by k, s, _;])]]