[STATEMENT]
lemma prv_LLq_Num_dsj:  \<comment> \<open>O8\<close>
assumes [simp]: "t \<in> atrm"
shows "prv (dsj (LLq t (Num n)) (LLq (Num n) t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (dsj (LLq t (Num n)) (LLq (Num n) t))
[PROOF STEP]
proof(induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))
 2. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))
 2. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
note prv_LLq_zer[simp]
[PROOF STATE]
proof (state)
this:
?t \<in> atrm \<Longrightarrow> prv (LLq zer ?t)

goal (2 subgoals):
 1. prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))
 2. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))
[PROOF STEP]
by (nprover3 r1: nprv_prvI r2: nprv_dsjIR r3: prv_nprvI)
[PROOF STATE]
proof (state)
this:
prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))

goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
prv (dsj (LLq t (Num n)) (LLq (Num n) t))

goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
have nn: "suc (Num n) = Num (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suc (Num n) = Num (Suc n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
suc (Num n) = Num (Suc n)

goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
have [simp]: "prv (LLq (Num n) (suc (Num n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (LLq (Num n) (suc (Num n)))
[PROOF STEP]
apply(subst nn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (LLq (Num n) (Num (Suc n)))
[PROOF STEP]
by (rule leq_prv_LLq_Num) simp
[PROOF STATE]
proof (state)
this:
prv (LLq (Num n) (suc (Num n)))

goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
apply(nrule r: nprv_prvI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule r: nprv_addLemmaE[OF Suc.IH])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule r: nprv_dsjE0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nprv {LLq t (Num n), dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
 2. nprv {LLq (Num n) t, dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq t (Num n), dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
by (nprover2 r1: nprv_dsjIL r2: O6I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (Num n) t, dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (Num n) t, dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule r: nprv_clear2_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule2 r: nprv_eql_Num_casesE[of t n])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nprv {eql t (Num n), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
 2. nprv {neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql t (Num n), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
by (nprover3 r1: nprv_dsjIL
      r2: nprv_eql_substE[of _ t "Num n" "LLq (Var xx) (suc (Num n))" xx]
      r3: prv_nprvI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule r: O7E0[of n t])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nprv {eql (Num n) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
 2. nprv {LLq (suc (Num n)) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql (Num n) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
by (nprover2 r1: nprv_eql_symE0 r2: nprv_negE01 )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (suc (Num n)) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (suc (Num n)) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
by (nrule r: nprv_dsjIR)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))

goal:
No subgoals!
[PROOF STEP]
qed