theory IterativeUnboundedNaturalAddDecBug_Add

imports Main

begin

lemma 1:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0
 |]
 ==>
    n_0 + m_0 = n_0 + m_0"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 2:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0
 |]
 ==>
    0 + m_0 = 0 + m_0"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 3:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0
 |]
 ==>
    0 = 0"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 4:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0
 |]
 ==>
    (~m_0 = 0 --> m_0 > 0)"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 5:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0 ;
    ~(m_2::int) = 0 ;
    (n_2::int) >= 0 ;
    m_2 >= 0 ;
    (k_2::int) >= 0 ;
    n_2 + m_2 = n_0 + m_0 ;
    k_2 + m_2 = 0 + m_0 ;
    n_2 + 1 >= 0 ;
    k_2 + 1 >= 0
 |]
 ==>
    n_2 + 1 + m_2 = n_0 + m_0"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 6:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0 ;
    ~(m_2::int) = 0 ;
    (n_2::int) >= 0 ;
    m_2 >= 0 ;
    (k_2::int) >= 0 ;
    n_2 + m_2 = n_0 + m_0 ;
    k_2 + m_2 = 0 + m_0 ;
    n_2 + 1 >= 0 ;
    k_2 + 1 >= 0
 |]
 ==>
    k_2 + 1 + m_2 = 0 + m_0"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 7:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0 ;
    ~(m_2::int) = 0 ;
    (n_2::int) >= 0 ;
    m_2 >= 0 ;
    (k_2::int) >= 0 ;
    n_2 + m_2 = n_0 + m_0 ;
    k_2 + m_2 = 0 + m_0 ;
    n_2 + 1 >= 0 ;
    k_2 + 1 >= 0
 |]
 ==>
    0 = 0"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 8:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0 ;
    ~(m_2::int) = 0 ;
    (n_2::int) >= 0 ;
    m_2 >= 0 ;
    (k_2::int) >= 0 ;
    n_2 + m_2 = n_0 + m_0 ;
    k_2 + m_2 = 0 + m_0 ;
    n_2 + 1 >= 0 ;
    k_2 + 1 >= 0
 |]
 ==>
    m_2 >= 0"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 9:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0 ;
    ~(m_2::int) = 0 ;
    (n_2::int) >= 0 ;
    m_2 >= 0 ;
    (k_2::int) >= 0 ;
    n_2 + m_2 = n_0 + m_0 ;
    k_2 + m_2 = 0 + m_0 ;
    n_2 + 1 >= 0 ;
    k_2 + 1 >= 0
 |]
 ==>
    m_2 < m_2"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 10:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0 ;
    (n_5::int) >= 0 ;
    (k_5::int) >= 0 ;
    n_5 + 0 = n_0 + m_0 ;
    k_5 + 0 = 0 + m_0
 |]
 ==>
    k_5 = m_0"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

lemma 11:

"[|
    (n_0::int) >= 0 ;
    (m_0::int) >= 0 ;
    0 >= 0 ;
    (n_5::int) >= 0 ;
    (k_5::int) >= 0 ;
    n_5 + 0 = n_0 + m_0 ;
    k_5 + 0 = 0 + m_0
 |]
 ==>
    n_5 = n_0 + k_5"

apply (((simp only: simp_thms),clarify?)+)?

apply (force+)?

done

end