[STATEMENT]
lemma nat_to_sch_2: "c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst
[PROOF STEP]
assume A1: "c_fst n mod 7 = 2"
[PROOF STATE]
proof (state)
this:
c_fst n mod 7 = 2

goal (1 subgoal):
 1. c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_fst n mod 7 = 2
[PROOF STEP]
have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)"
[PROOF STATE]
proof (prove)
using this:
c_fst n mod 7 = 2

goal (1 subgoal):
 1. nat_to_sch n = (let u = c_fst n mod 7; v = c_snd n; v1 = c_fst v; v2 = c_snd v; sch1 = nat_to_sch v1 in Let (nat_to_sch v2) (loc_f u sch1))
[PROOF STEP]
by (simp add: loc_lm_2)
[PROOF STATE]
proof (state)
this:
nat_to_sch n = (let u = c_fst n mod 7; v = c_snd n; v1 = c_fst v; v2 = c_snd v; sch1 = nat_to_sch v1 in Let (nat_to_sch v2) (loc_f u sch1))

goal (1 subgoal):
 1. c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst
[PROOF STEP]
with A1
[PROOF STATE]
proof (chain)
picking this:
c_fst n mod 7 = 2
nat_to_sch n = (let u = c_fst n mod 7; v = c_snd n; v1 = c_fst v; v2 = c_snd v; sch1 = nat_to_sch v1 in Let (nat_to_sch v2) (loc_f u sch1))
[PROOF STEP]
show "nat_to_sch n = Base_fst"
[PROOF STATE]
proof (prove)
using this:
c_fst n mod 7 = 2
nat_to_sch n = (let u = c_fst n mod 7; v = c_snd n; v1 = c_fst v; v2 = c_snd v; sch1 = nat_to_sch v1 in Let (nat_to_sch v2) (loc_f u sch1))

goal (1 subgoal):
 1. nat_to_sch n = Base_fst
[PROOF STEP]
by (simp add: Let_def loc_f_def)
[PROOF STATE]
proof (state)
this:
nat_to_sch n = Base_fst

goal:
No subgoals!
[PROOF STEP]
qed