theory RecursiveUnboundedNaturalMultiplyIncBug_Multiply

imports Main

begin

lemma 1:

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

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

apply (force+)?

done

lemma 2:

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

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

apply (force+)?

done

lemma 3:

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

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

apply (force+)?

done

lemma 4:

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

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

apply (force+)?

done

lemma 5:

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

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

apply (force+)?

done

lemma 6:

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

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

apply (force+)?

done

lemma 7:

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

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

apply (force+)?

done

lemma 8:

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

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

apply (force+)?

done

lemma 9:

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

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

apply (force+)?

done

end