[STATEMENT]
theorem gb_schema_direct_pmdl:
  assumes "struct_spec sel ap ab compl" and "compl_pmdl compl"
  shows "pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)
[PROOF STEP]
have "pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) =
          pmdl (fst ` set ([] @ (fst (add_indices (bs, data) (0, data)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))
[PROOF STEP]
unfolding fst_gb_schema_direct Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_aux sel ap ab compl [] (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data) (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (ap [] [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)))) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
struct_spec sel ap ab compl
compl_pmdl compl

goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_aux sel ap ab compl [] (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data) (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (ap [] [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)))) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))
[PROOF STEP]
proof (rule gb_schema_aux_pmdl_init)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. is_Groebner_basis (fst ` set [])
 2. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 3. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
from is_Groebner_basis_empty
[PROOF STATE]
proof (chain)
picking this:
is_Groebner_basis {}
[PROOF STEP]
show "is_Groebner_basis (fst ` set [])"
[PROOF STATE]
proof (prove)
using this:
is_Groebner_basis {}

goal (1 subgoal):
 1. is_Groebner_basis (fst ` set [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_Groebner_basis (fst ` set [])

goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
let ?data = "(length bs, data)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
struct_spec sel ap ab compl
[PROOF STEP]
have "ab_spec ab"
[PROOF STATE]
proof (prove)
using this:
struct_spec sel ap ab compl

goal (1 subgoal):
 1. ab_spec ab
[PROOF STEP]
by (rule struct_specD)
[PROOF STATE]
proof (state)
this:
ab_spec ab

goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab_spec ab

goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
have "unique_idx ([] @ []) (0, data)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unique_idx ([] @ []) (0, data)
[PROOF STEP]
by (simp add: unique_idx_Nil)
[PROOF STATE]
proof (state)
this:
unique_idx ([] @ []) (0, data)

goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ab_spec ab
unique_idx ([] @ []) (0, data)
[PROOF STEP]
show "unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) ?data) ?data"
[PROOF STATE]
proof (prove)
using this:
ab_spec ab
unique_idx ([] @ []) (0, data)

goal (1 subgoal):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
[PROOF STEP]
proof (rule unique_idx_ab)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices ?aux (0, data)
[PROOF STEP]
show "(fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices (bs, data) (0, data)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices (bs, data) (0, data)
[PROOF STEP]
by (simp add: add_indices_def)
[PROOF STATE]
proof (state)
this:
(fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices (bs, data) (0, data)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)

goal (1 subgoal):
 1. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
qed (simp add: rem_comps_spec_count_rem_components)
[PROOF STATE]
proof (state)
this:
pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))

goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))

goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)
[PROOF STEP]
by (simp add: fst_set_add_indices)
[PROOF STATE]
proof (state)
this:
pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)

goal:
No subgoals!
[PROOF STEP]
qed