[STATEMENT]
lemma "\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
have "?thesis = eval_pf (Forall (Exist (Or (Eq [1, -1] 5)
    (Forall (Forall (Imp (Neg (Le [-1, 0] (- 6))) (Imp (Eq [1, 6, 0, -1] 0) (Eq [0, 1] 1)))))))) []"
    (is "_ = eval_pf ?P []")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)) = eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)) = eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)) = eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
have "\<dots> = dfa_accepts (dfa_of_pf 0 ?P) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) [] = dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []
[PROOF STEP]
by (simp add: dfa_of_pf_correctness del: dfa_of_pf.simps)
[PROOF STATE]
proof (state)
this:
eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) [] = dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) [] = dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
have "\<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)

goal:
No subgoals!
[PROOF STEP]
qed