Proof Summary of Lambda.thy:161

Isabelle Statement

source: Lambda.thy:161 benchmark: isa/deeper/B-mesh-th0/train2k problem: problems/HOL-Proofs-Lambda/0002_Lambda/prob_00161_004528.p

Lemma

theorem subst_preserves_beta': "r →_β^* s ⟹ r[t/i] →_β^* s[t/i]"

Proof Excerpt

theorem subst_preserves_beta': "r →_β^* s ⟹ r[t/i] →_β^* s[t/i]"
proof (induct set: rtranclp)
  case base
  then show ?case
    by (iprover intro: rtrancl_refl)

Conjectures

c_0_0

transi72828568clp_dB @ beta @ ( subst @ r @ t @ i ) @ ( subst @ r @ t @ i )

Axioms

c_0_1

Final Contradiction

c_0_8