Loading theory "Diophantine_Eqns_Lin_Hom.List_Vector"
Loading theory "Diophantine_Eqns_Lin_Hom.Sorted_Wrt"
Proofs for inductive predicate(s) "sorted_wrt"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Diophantine_Eqns_Lin_Hom.Sorted_Wrt"
### 0.209s elapsed time, 0.492s cpu time, 0.000s GC time
Loading theory "Diophantine_Eqns_Lin_Hom.Minimize_Wrt"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "Diophantine_Eqns_Lin_Hom.Minimize_Wrt"
### 0.231s elapsed time, 0.464s cpu time, 0.000s GC time
Found termination order:
  "(\<lambda>p. length (snd (snd (snd p)))) <*mlex*> {}"
### theory "Diophantine_Eqns_Lin_Hom.List_Vector"
### 0.928s elapsed time, 1.896s cpu time, 0.000s GC time
Loading theory "Diophantine_Eqns_Lin_Hom.Linear_Diophantine_Equations"
locale
 
hlde_ops


fixes a :: "nat list" 
  and b :: "nat list" 
locale
 
hlde


fixes a :: "nat list" 
  and b :: "nat list" 


assumes "hlde a b"
### theory "Diophantine_Eqns_Lin_Hom.Linear_Diophantine_Equations"
### 0.914s elapsed time, 1.808s cpu time, 0.280s GC time
Loading theory "Diophantine_Eqns_Lin_Hom.Algorithm"
Found termination order: "{}"
### The following clauses are redundant (covered by preceding clauses):
### x \<Rightarrow> []
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
locale
 
bounded_lexs


fixes C :: "nat list \<Rightarrow> nat \<Rightarrow> bool" 
  and B :: "nat" 


assumes "bounded_lexs C B"
Found termination order: "size_list size <*mlex*> {}"
locale
 
bounded_lexs2


fixes C\<^sub>2 :: "nat list \<Rightarrow> nat \<Rightarrow> bool" 
  and B\<^sub>2 :: "nat" 
  and
  C\<^sub>1 ::
    "nat list
     \<Rightarrow> nat list
                   \<Rightarrow> nat list
                                 \<Rightarrow> nat \<Rightarrow> bool"
    
  and B\<^sub>1 :: "nat list \<Rightarrow> nat" 


assumes "bounded_lexs2 C\<^sub>2 B\<^sub>2 C\<^sub>1 B\<^sub>1"
Found termination order: "{}"
Found termination order: "{}"
locale
 
bounded_incs


fixes cond :: "nat list \<Rightarrow> nat \<Rightarrow> bool" 
  and B :: "nat" 


assumes "bounded_incs cond B"
Found termination order:
  "(\<lambda>p. size_list size (snd (snd p))) <*mlex*> {}"
### theory "Diophantine_Eqns_Lin_Hom.Algorithm"
### 2.779s elapsed time, 5.532s cpu time, 0.248s GC time
### Metis: Unused theorems: "Divides.unique_euclidean_semiring_numeral_class.div_positive"
*** Interrupt