Package hol-ring: HOL ring theories
Information
| name | hol-ring |
| version | 1.1 |
| description | HOL ring theories |
| author | HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> |
| license | MIT |
| checksum | 7846e439537b4532a7e848e4764e13b599b8e40e |
| requires | base hol-base |
| show | Data.Bool Data.List Data.Pair Function HOL4 Number.Natural Relation |
Files
- Package tarball hol-ring-1.1.tgz
- Theory source file hol-ring.thy (included in the package tarball)
Defined Type Operators
- HOL4
- canonical
- canonical.canonical_sum
- canonical.spolynom
- prelim
- prelim.ordering
- quote
- quote.index
- quote.varmap
- ring
- ring.ring
- ringNorm
- ringNorm.polynom
- semi_ring
- semi_ring.semi_ring
- canonical
Defined Constants
- HOL4
- canonical
- canonical.canonical_sum_CASE
- canonical.canonical_sum_merge
- canonical.canonical_sum_prod
- canonical.canonical_sum_scalar
- canonical.canonical_sum_scalar2
- canonical.canonical_sum_scalar3
- canonical.canonical_sum_simplify
- canonical.canonical_sum_size
- canonical.ics_aux
- canonical.interp_cs
- canonical.interp_m
- canonical.interp_sp
- canonical.interp_vl
- canonical.ivl_aux
- canonical.monom_insert
- canonical.spolynom_CASE
- canonical.spolynom_normalize
- canonical.spolynom_simplify
- canonical.spolynom_size
- canonical.varlist_insert
- canonical.Cons_monom
- canonical.Cons_varlist
- canonical.Nil_monom
- canonical.SPconst
- canonical.SPmult
- canonical.SPplus
- canonical.SPvar
- numRing
- numRing.num_canonical_sum_merge
- numRing.num_canonical_sum_prod
- numRing.num_canonical_sum_scalar
- numRing.num_canonical_sum_scalar2
- numRing.num_canonical_sum_scalar3
- numRing.num_canonical_sum_simplify
- numRing.num_ics_aux
- numRing.num_interp_cs
- numRing.num_interp_m
- numRing.num_interp_sp
- numRing.num_interp_vl
- numRing.num_ivl_aux
- numRing.num_monom_insert
- numRing.num_spolynom_normalize
- numRing.num_spolynom_simplify
- numRing.num_varlist_insert
- prelim
- prelim.compare
- prelim.list_compare
- prelim.list_compare_tupled
- prelim.list_merge
- prelim.list_merge_tupled
- prelim.num2ordering
- prelim.ordering2num
- prelim.ordering_CASE
- prelim.ordering_size
- prelim.EQUAL
- prelim.GREATER
- prelim.LESS
- quote
- quote.index_CASE
- quote.index_compare
- quote.index_lt
- quote.index_size
- quote.varmap_CASE
- quote.varmap_find
- quote.varmap_find_tupled
- quote.varmap_size
- quote.Empty_vm
- quote.End_idx
- quote.Left_idx
- quote.Node_vm
- quote.Right_idx
- ring
- ring.is_ring
- ring.recordtype.ring
- ring.ring_CASE
- ring.ring_R0
- ring.ring_R0_fupd
- ring.ring_R1
- ring.ring_R1_fupd
- ring.ring_RM
- ring.ring_RM_fupd
- ring.ring_RN
- ring.ring_RN_fupd
- ring.ring_RP
- ring.ring_RP_fupd
- ring.ring_size
- ring.semi_ring_of
- ringNorm
- ringNorm.interp_p
- ringNorm.polynom_CASE
- ringNorm.polynom_normalize
- ringNorm.polynom_simplify
- ringNorm.polynom_size
- ringNorm.r_canonical_sum_merge
- ringNorm.r_canonical_sum_prod
- ringNorm.r_canonical_sum_scalar
- ringNorm.r_canonical_sum_scalar2
- ringNorm.r_canonical_sum_scalar3
- ringNorm.r_canonical_sum_simplify
- ringNorm.r_ics_aux
- ringNorm.r_interp_cs
- ringNorm.r_interp_m
- ringNorm.r_interp_sp
- ringNorm.r_interp_vl
- ringNorm.r_ivl_aux
- ringNorm.r_monom_insert
- ringNorm.r_spolynom_normalize
- ringNorm.r_spolynom_simplify
- ringNorm.r_varlist_insert
- ringNorm.Pconst
- ringNorm.Pmult
- ringNorm.Popp
- ringNorm.Pplus
- ringNorm.Pvar
- semi_ring
- semi_ring.is_semi_ring
- semi_ring.recordtype.semi_ring
- semi_ring.semi_ring_CASE
- semi_ring.semi_ring_SR0
- semi_ring.semi_ring_SR0_fupd
- semi_ring.semi_ring_SR1
- semi_ring.semi_ring_SR1_fupd
- semi_ring.semi_ring_SRM
- semi_ring.semi_ring_SRM_fupd
- semi_ring.semi_ring_SRP
- semi_ring.semi_ring_SRP_fupd
- semi_ring.semi_ring_size
- canonical
Theorems
⊦ prelim.LESS = prelim.num2ordering 0
⊦ prelim.EQUAL = prelim.num2ordering 1
⊦ prelim.GREATER = prelim.num2ordering (arithmetic.BIT2 0)
⊦ ∀x. prelim.ordering_size x = 0
⊦ ∀a. prelim.num2ordering (prelim.ordering2num a) = a
⊦ semi_ring.is_semi_ring (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ ∀r.
ringNorm.r_canonical_sum_simplify r =
canonical.canonical_sum_simplify (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_spolynom_normalize r =
canonical.spolynom_normalize (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_spolynom_simplify r =
canonical.spolynom_simplify (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_canonical_sum_scalar r =
canonical.canonical_sum_scalar (ring.semi_ring_of r)
⊦ ∀r. ringNorm.r_interp_vl r = canonical.interp_vl (ring.semi_ring_of r)
⊦ ∀r. ringNorm.r_interp_cs r = canonical.interp_cs (ring.semi_ring_of r)
⊦ ∀r. ringNorm.r_interp_sp r = canonical.interp_sp (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_canonical_sum_scalar2 r =
canonical.canonical_sum_scalar2 (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_varlist_insert r =
canonical.varlist_insert (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_canonical_sum_merge r =
canonical.canonical_sum_merge (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_canonical_sum_prod r =
canonical.canonical_sum_prod (ring.semi_ring_of r)
⊦ ∀r. ringNorm.r_interp_m r = canonical.interp_m (ring.semi_ring_of r)
⊦ ∀r. ringNorm.r_ics_aux r = canonical.ics_aux (ring.semi_ring_of r)
⊦ ∀r. ringNorm.r_ivl_aux r = canonical.ivl_aux (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_canonical_sum_scalar3 r =
canonical.canonical_sum_scalar3 (ring.semi_ring_of r)
⊦ ∀r.
ringNorm.r_monom_insert r =
canonical.monom_insert (ring.semi_ring_of r)
⊦ ∀r. ring.is_ring r ⇒ semi_ring.is_semi_ring (ring.semi_ring_of r)
⊦ ∃rep. bool.TYPE_DEFINITION (λn. n < 3) rep
⊦ numRing.num_canonical_sum_simplify =
canonical.canonical_sum_simplify
(semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_spolynom_normalize =
canonical.spolynom_normalize (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_spolynom_simplify =
canonical.spolynom_simplify (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_canonical_sum_scalar =
canonical.canonical_sum_scalar
(semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_interp_vl =
canonical.interp_vl (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_interp_cs =
canonical.interp_cs (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_interp_sp =
canonical.interp_sp (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_canonical_sum_scalar2 =
canonical.canonical_sum_scalar2
(semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_varlist_insert =
canonical.varlist_insert (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_canonical_sum_merge =
canonical.canonical_sum_merge
(semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_canonical_sum_prod =
canonical.canonical_sum_prod (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_ivl_aux =
canonical.ivl_aux (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_interp_m =
canonical.interp_m (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_ics_aux =
canonical.ics_aux (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_canonical_sum_scalar3 =
canonical.canonical_sum_scalar3
(semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ numRing.num_monom_insert =
canonical.monom_insert (semi_ring.recordtype.semi_ring 0 1 (+) (*))
⊦ ∀x x1. quote.varmap_find x x1 = quote.varmap_find_tupled (x, x1)
⊦ ∀a2 a1 a0. ¬(quote.Empty_vm = quote.Node_vm a0 a1 a2)
⊦ ∀a a'. a = a' ⇔ prelim.ordering2num a = prelim.ordering2num a'
⊦ ∀a a'. prelim.ordering2num a = prelim.ordering2num a' ⇔ a = a'
⊦ ∀i1 i2. quote.index_lt i1 i2 ⇔ quote.index_compare i1 i2 = prelim.LESS
⊦ ∀i1 i2. quote.index_compare i1 i2 = prelim.EQUAL ⇔ i1 = i2
⊦ ∀r x.
ringNorm.r_spolynom_simplify r x =
ringNorm.r_canonical_sum_simplify r (ringNorm.r_spolynom_normalize r x)
⊦ ∀r x.
ringNorm.polynom_simplify r x =
ringNorm.r_canonical_sum_simplify r (ringNorm.polynom_normalize r x)
⊦ ∀sr x.
canonical.spolynom_simplify sr x =
canonical.canonical_sum_simplify sr (canonical.spolynom_normalize sr x)
⊦ ∀a. a = prelim.LESS ∨ a = prelim.EQUAL ∨ a = prelim.GREATER
⊦ ∀r. r < 3 ⇔ prelim.ordering2num (prelim.num2ordering r) = r
⊦ ∀a. ∃r. a = prelim.num2ordering r ∧ r < 3
⊦ ∀r. r < 3 ⇔ ∃a. r = prelim.ordering2num a
⊦ ∀l1 l2.
prelim.list_compare quote.index_compare l1 l2 = prelim.EQUAL ⇔ l1 = l2
⊦ ∀r. ring.is_ring r ⇒ ∀n. ring.ring_RM r n (ring.ring_R1 r) = n
⊦ ∀r. ring.is_ring r ⇒ ∀n. ring.ring_RP r n (ring.ring_R0 r) = n
⊦ ∀r. ring.is_ring r ⇒ ∀n. ring.ring_RM r (ring.ring_R1 r) n = n
⊦ ∀r. ring.is_ring r ⇒ ∀n. ring.ring_RP r (ring.ring_R0 r) n = n
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n. semi_ring.semi_ring_SRM r n (semi_ring.semi_ring_SR1 r) = n
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n. semi_ring.semi_ring_SRP r n (semi_ring.semi_ring_SR0 r) = n
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n. semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SR1 r) n = n
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n. semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SR0 r) n = n
⊦ ∀r.
ring.semi_ring_of r =
semi_ring.recordtype.semi_ring (ring.ring_R0 r) (ring.ring_R1 r)
(ring.ring_RP r) (ring.ring_RM r)
⊦ ∀a a0 f f0.
semi_ring.semi_ring_SR0 (semi_ring.recordtype.semi_ring a a0 f f0) = a
⊦ ∀a a0 f f0.
semi_ring.semi_ring_SR1 (semi_ring.recordtype.semi_ring a a0 f f0) = a0
⊦ ∀a a0 f f0.
semi_ring.semi_ring_SRM (semi_ring.recordtype.semi_ring a a0 f f0) = f0
⊦ ∀a a0 f f0.
semi_ring.semi_ring_SRP (semi_ring.recordtype.semi_ring a a0 f f0) = f
⊦ ∀r.
ring.is_ring r ⇒ ∀n. ring.ring_RM r n (ring.ring_R0 r) = ring.ring_R0 r
⊦ ∀r.
ring.is_ring r ⇒ ∀n. ring.ring_RM r (ring.ring_R0 r) n = ring.ring_R0 r
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n.
semi_ring.semi_ring_SRM r n (semi_ring.semi_ring_SR0 r) =
semi_ring.semi_ring_SR0 r
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n.
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SR0 r) n =
semi_ring.semi_ring_SR0 r
⊦ ∀P. P prelim.EQUAL ∧ P prelim.GREATER ∧ P prelim.LESS ⇒ ∀a. P a
⊦ ¬(prelim.LESS = prelim.EQUAL) ∧ ¬(prelim.LESS = prelim.GREATER) ∧
¬(prelim.EQUAL = prelim.GREATER)
⊦ ∀x. ∃a a0 f f0. x = semi_ring.recordtype.semi_ring a a0 f f0
⊦ ∀r.
ring.is_ring r ⇒
∀n. ring.ring_RP r n (ring.ring_RN r n) = ring.ring_R0 r
⊦ ∀x x1 x2.
prelim.list_merge x x1 x2 = prelim.list_merge_tupled (x, x1, x2)
⊦ ∀x x1 x2.
prelim.list_compare x x1 x2 = prelim.list_compare_tupled (x, x1, x2)
⊦ ∀vv. vv = quote.Empty_vm ∨ ∃a v v0. vv = quote.Node_vm a v v0
⊦ prelim.num2ordering 0 = prelim.LESS ∧
prelim.num2ordering 1 = prelim.EQUAL ∧
prelim.num2ordering (arithmetic.BIT2 0) = prelim.GREATER
⊦ prelim.ordering2num prelim.LESS = 0 ∧
prelim.ordering2num prelim.EQUAL = 1 ∧
prelim.ordering2num prelim.GREATER = arithmetic.BIT2 0
⊦ ∀a a0 f f0 f1. ring.ring_R0 (ring.recordtype.ring a a0 f f0 f1) = a
⊦ ∀a a0 f f0 f1. ring.ring_R1 (ring.recordtype.ring a a0 f f0 f1) = a0
⊦ ∀a a0 f f0 f1. ring.ring_RN (ring.recordtype.ring a a0 f f0 f1) = f1
⊦ ∀a a0 f f0 f1. ring.ring_RM (ring.recordtype.ring a a0 f f0 f1) = f0
⊦ ∀a a0 f f0 f1. ring.ring_RP (ring.recordtype.ring a a0 f f0 f1) = f
⊦ ∀r. ring.is_ring r ⇒ ∀n m. ring.ring_RM r n m = ring.ring_RM r m n
⊦ ∀r. ring.is_ring r ⇒ ∀n m. ring.ring_RP r n m = ring.ring_RP r m n
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n m. semi_ring.semi_ring_SRM r n m = semi_ring.semi_ring_SRM r m n
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n m. semi_ring.semi_ring_SRP r n m = semi_ring.semi_ring_SRP r m n
⊦ ∀x. ∃a a0 f f0 f1. x = ring.recordtype.ring a a0 f f0 f1
⊦ ∀ii.
(∃i. ii = quote.Left_idx i) ∨ (∃i. ii = quote.Right_idx i) ∨
ii = quote.End_idx
⊦ ∀P.
(∀a0 a1 a2 a3. P (semi_ring.recordtype.semi_ring a0 a1 a2 a3)) ⇒
∀x. P x
⊦ ∀r.
ring.is_ring r ⇒
∀vm p.
ringNorm.r_interp_cs r vm (ringNorm.polynom_normalize r p) =
ringNorm.interp_p r vm p
⊦ ∀r.
ring.is_ring r ⇒
∀vm p.
ringNorm.r_interp_cs r vm (ringNorm.polynom_simplify r p) =
ringNorm.interp_p r vm p
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm s.
canonical.interp_cs sr vm (canonical.canonical_sum_simplify sr s) =
canonical.interp_cs sr vm s
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm p.
canonical.interp_cs sr vm (canonical.spolynom_normalize sr p) =
canonical.interp_sp sr vm p
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm p.
canonical.interp_cs sr vm (canonical.spolynom_simplify sr p) =
canonical.interp_sp sr vm p
⊦ ∀x0 x1 x2.
∃f. f prelim.LESS = x0 ∧ f prelim.EQUAL = x1 ∧ f prelim.GREATER = x2
⊦ ∀a0 a1 a2 a3 f.
semi_ring.semi_ring_CASE (semi_ring.recordtype.semi_ring a0 a1 a2 a3)
f = f a0 a1 a2 a3
⊦ ∀r.
ring.is_ring r ⇒
∀a b.
ring.ring_RM r (ring.ring_RN r a) b =
ring.ring_RN r (ring.ring_RM r a b)
⊦ ∀P. (∀a0 a1 a2 a3 a4. P (ring.recordtype.ring a0 a1 a2 a3 a4)) ⇒ ∀x. P x
⊦ ∀f.
∃fn.
∀a0 a1 a2 a3.
fn (semi_ring.recordtype.semi_ring a0 a1 a2 a3) = f a0 a1 a2 a3
⊦ ∀f1 a a0 f f0.
semi_ring.semi_ring_SR0_fupd f1
(semi_ring.recordtype.semi_ring a a0 f f0) =
semi_ring.recordtype.semi_ring (f1 a) a0 f f0
⊦ ∀f1 a a0 f f0.
semi_ring.semi_ring_SR1_fupd f1
(semi_ring.recordtype.semi_ring a a0 f f0) =
semi_ring.recordtype.semi_ring a (f1 a0) f f0
⊦ ∀f1 a a0 f f0.
semi_ring.semi_ring_SRM_fupd f1
(semi_ring.recordtype.semi_ring a a0 f f0) =
semi_ring.recordtype.semi_ring a a0 f (f1 f0)
⊦ ∀f1 a a0 f f0.
semi_ring.semi_ring_SRP_fupd f1
(semi_ring.recordtype.semi_ring a a0 f f0) =
semi_ring.recordtype.semi_ring a a0 (f1 f) f0
⊦ (∀a. prelim.num2ordering (prelim.ordering2num a) = a) ∧
∀r.
(let n ← r in n < 3) ⇔ prelim.ordering2num (prelim.num2ordering r) = r
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm x l.
canonical.interp_m sr vm x l =
semi_ring.semi_ring_SRM sr x (canonical.interp_vl sr vm l)
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm x s.
canonical.ics_aux sr vm x s =
semi_ring.semi_ring_SRP sr x (canonical.interp_cs sr vm s)
⊦ ∀s.
∃a0 a f0 f.
s =
semi_ring.semi_ring_SR0_fupd (const a0)
(semi_ring.semi_ring_SR1_fupd (const a)
(semi_ring.semi_ring_SRP_fupd (const f0)
(semi_ring.semi_ring_SRM_fupd (const f) bool.ARB)))
⊦ ∀f a0 a1 a2 a3.
semi_ring.semi_ring_size f
(semi_ring.recordtype.semi_ring a0 a1 a2 a3) = 1 + (f a0 + f a1)
⊦ ∀a0 a1 a2 a3 a4 f.
ring.ring_CASE (ring.recordtype.ring a0 a1 a2 a3 a4) f =
f a0 a1 a2 a3 a4
⊦ ∀r r'.
r < 3 ⇒ r' < 3 ⇒
(prelim.num2ordering r = prelim.num2ordering r' ⇔ r = r')
⊦ ∀r.
ring.is_ring r ⇒
∀n m p.
ring.ring_RM r n (ring.ring_RM r m p) =
ring.ring_RM r (ring.ring_RM r n m) p
⊦ ∀r.
ring.is_ring r ⇒
∀n m p.
ring.ring_RP r n (ring.ring_RP r m p) =
ring.ring_RP r (ring.ring_RP r n m) p
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n m p.
semi_ring.semi_ring_SRM r n (semi_ring.semi_ring_SRM r m p) =
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r n m) p
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n m p.
semi_ring.semi_ring_SRP r n (semi_ring.semi_ring_SRP r m p) =
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r n m) p
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀m n p.
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r m n) p =
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r m p) n
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀m n p.
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r m n) p =
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r n p) m
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀m n p.
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r m n) p =
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r m p) n
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀m n p.
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r m n) p =
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r n p) m
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm a s.
canonical.interp_cs sr vm (canonical.canonical_sum_scalar sr a s) =
semi_ring.semi_ring_SRM sr a (canonical.interp_cs sr vm s)
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm v i.
canonical.ivl_aux sr vm i v =
semi_ring.semi_ring_SRM sr (quote.varmap_find i vm)
(canonical.interp_vl sr vm v)
⊦ (∀a' a. ¬(quote.Left_idx a = quote.Right_idx a')) ∧
(∀a. ¬(quote.Left_idx a = quote.End_idx)) ∧
∀a. ¬(quote.Right_idx a = quote.End_idx)
⊦ ∀P.
P quote.Empty_vm ∧
(∀a1 a2. P a1 ∧ P a2 ⇒ ∀a0. P (quote.Node_vm a0 a1 a2)) ⇒ ∀v1. P v1
⊦ ∀f.
∃fn.
∀a0 a1 a2 a3 a4.
fn (ring.recordtype.ring a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4
⊦ ∀cc.
cc = canonical.Nil_monom ∨ (∃a l c. cc = canonical.Cons_monom a l c) ∨
∃l c. cc = canonical.Cons_varlist l c
⊦ ∀f2 a a0 f f0 f1.
ring.ring_R0_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring (f2 a) a0 f f0 f1
⊦ ∀f2 a a0 f f0 f1.
ring.ring_R1_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring a (f2 a0) f f0 f1
⊦ ∀P.
(∀i. P i ⇒ P (quote.Left_idx i)) ∧ (∀i. P i ⇒ P (quote.Right_idx i)) ∧
P quote.End_idx ⇒ ∀i1. P i1
⊦ ∀f2 a a0 f f0 f1.
ring.ring_RN_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring a a0 f f0 (f2 f1)
⊦ ∀f2 a a0 f f0 f1.
ring.ring_RM_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring a a0 f (f2 f0) f1
⊦ ∀f2 a a0 f f0 f1.
ring.ring_RP_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring a a0 (f2 f) f0 f1
⊦ (∀a a'. quote.Left_idx a = quote.Left_idx a' ⇔ a = a') ∧
∀a a'. quote.Right_idx a = quote.Right_idx a' ⇔ a = a'
⊦ ∀f a0 a1 a2 a3 a4.
ring.ring_size f (ring.recordtype.ring a0 a1 a2 a3 a4) =
1 + (f a0 + f a1)
⊦ ∀P.
(∀x. P x) ⇔
∀a0 a f0 f.
P
(semi_ring.semi_ring_SR0_fupd (const a0)
(semi_ring.semi_ring_SR1_fupd (const a)
(semi_ring.semi_ring_SRP_fupd (const f0)
(semi_ring.semi_ring_SRM_fupd (const f) bool.ARB))))
⊦ ∀P.
(∃x. P x) ⇔
∃a0 a f0 f.
P
(semi_ring.semi_ring_SR0_fupd (const a0)
(semi_ring.semi_ring_SR1_fupd (const a)
(semi_ring.semi_ring_SRP_fupd (const f0)
(semi_ring.semi_ring_SRM_fupd (const f) bool.ARB))))
⊦ (∀x y. cmp x y = prelim.EQUAL ⇔ x = y) ⇒
∀l1 l2. prelim.list_compare cmp l1 l2 = prelim.EQUAL ⇔ l1 = l2
⊦ ∀r.
∃a0 a f1 f0 f.
r =
ring.ring_R0_fupd (const a0)
(ring.ring_R1_fupd (const a)
(ring.ring_RP_fupd (const f1)
(ring.ring_RM_fupd (const f0)
(ring.ring_RN_fupd (const f) bool.ARB))))
⊦ ∀r.
ring.is_ring r ⇒
∀n m p.
ring.ring_RM r (ring.ring_RP r n m) p =
ring.ring_RP r (ring.ring_RM r n p) (ring.ring_RM r m p)
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀m n p.
semi_ring.semi_ring_SRM r m (semi_ring.semi_ring_SRP r n p) =
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRM r m n)
(semi_ring.semi_ring_SRM r m p)
⊦ ∀r.
semi_ring.is_semi_ring r ⇒
∀n m p.
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRP r n m) p =
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRM r n p)
(semi_ring.semi_ring_SRM r m p)
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm x y.
canonical.interp_vl sr vm (prelim.list_merge quote.index_lt x y) =
semi_ring.semi_ring_SRM sr (canonical.interp_vl sr vm x)
(canonical.interp_vl sr vm y)
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm l s.
canonical.interp_cs sr vm (canonical.canonical_sum_scalar2 sr l s) =
semi_ring.semi_ring_SRM sr (canonical.interp_vl sr vm l)
(canonical.interp_cs sr vm s)
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm l s.
canonical.interp_cs sr vm (canonical.varlist_insert sr l s) =
semi_ring.semi_ring_SRP sr (canonical.interp_vl sr vm l)
(canonical.interp_cs sr vm s)
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm x y.
canonical.interp_cs sr vm (canonical.canonical_sum_merge sr x y) =
semi_ring.semi_ring_SRP sr (canonical.interp_cs sr vm x)
(canonical.interp_cs sr vm y)
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm x y.
canonical.interp_cs sr vm (canonical.canonical_sum_prod sr x y) =
semi_ring.semi_ring_SRM sr (canonical.interp_cs sr vm x)
(canonical.interp_cs sr vm y)
⊦ (∀a. quote.index_size (quote.Left_idx a) = 1 + quote.index_size a) ∧
(∀a. quote.index_size (quote.Right_idx a) = 1 + quote.index_size a) ∧
quote.index_size quote.End_idx = 0
⊦ ∀x v0 v1 v2.
prelim.ordering_CASE x v0 v1 v2 =
let m ← prelim.ordering2num x in
if m < 1 then v0 else if m = 1 then v1 else v2
⊦ ∀r.
(∀vm. ringNorm.r_interp_vl r vm [] = ring.ring_R1 r) ∧
∀vm x t.
ringNorm.r_interp_vl r vm (x :: t) = ringNorm.r_ivl_aux r vm x t
⊦ ∀f0 f1.
∃fn.
fn quote.Empty_vm = f0 ∧
∀a0 a1 a2. fn (quote.Node_vm a0 a1 a2) = f1 a0 a1 a2 (fn a1) (fn a2)
⊦ (∀sr vm. canonical.interp_vl sr vm [] = semi_ring.semi_ring_SR1 sr) ∧
∀sr vm x t.
canonical.interp_vl sr vm (x :: t) = canonical.ivl_aux sr vm x t
⊦ (∀v f. quote.varmap_CASE quote.Empty_vm v f = v) ∧
∀a0 a1 a2 v f.
quote.varmap_CASE (quote.Node_vm a0 a1 a2) v f = f a0 a1 a2
⊦ ∀a0 a1 a2 a0' a1' a2'.
quote.Node_vm a0 a1 a2 = quote.Node_vm a0' a1' a2' ⇔
a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
⊦ ∀s1 s2.
s1 = s2 ⇔
semi_ring.semi_ring_SR0 s1 = semi_ring.semi_ring_SR0 s2 ∧
semi_ring.semi_ring_SR1 s1 = semi_ring.semi_ring_SR1 s2 ∧
semi_ring.semi_ring_SRP s1 = semi_ring.semi_ring_SRP s2 ∧
semi_ring.semi_ring_SRM s1 = semi_ring.semi_ring_SRM s2
⊦ ∀P.
(∀x. P x) ⇔
∀a0 a f1 f0 f.
P
(ring.ring_R0_fupd (const a0)
(ring.ring_R1_fupd (const a)
(ring.ring_RP_fupd (const f1)
(ring.ring_RM_fupd (const f0)
(ring.ring_RN_fupd (const f) bool.ARB)))))
⊦ ∀P.
(∃x. P x) ⇔
∃a0 a f1 f0 f.
P
(ring.ring_R0_fupd (const a0)
(ring.ring_R1_fupd (const a)
(ring.ring_RP_fupd (const f1)
(ring.ring_RM_fupd (const f0)
(ring.ring_RN_fupd (const f) bool.ARB)))))
⊦ ∀f0 f1 f2.
∃fn.
(∀a. fn (quote.Left_idx a) = f0 a (fn a)) ∧
(∀a. fn (quote.Right_idx a) = f1 a (fn a)) ∧ fn quote.End_idx = f2
⊦ ∀x.
(∃i. x = canonical.SPvar i) ∨ (∃a. x = canonical.SPconst a) ∨
(∃s s0. x = canonical.SPplus s s0) ∨ ∃s s0. x = canonical.SPmult s s0
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm c l s.
canonical.interp_cs sr vm
(canonical.canonical_sum_scalar3 sr c l s) =
semi_ring.semi_ring_SRM sr
(semi_ring.semi_ring_SRM sr c (canonical.interp_vl sr vm l))
(canonical.interp_cs sr vm s)
⊦ ∀sr.
semi_ring.is_semi_ring sr ⇒
∀vm a l s.
canonical.interp_cs sr vm (canonical.monom_insert sr a l s) =
semi_ring.semi_ring_SRP sr
(semi_ring.semi_ring_SRM sr a (canonical.interp_vl sr vm l))
(canonical.interp_cs sr vm s)
⊦ ∀P.
P canonical.Nil_monom ∧
(∀c. P c ⇒ ∀l a. P (canonical.Cons_monom a l c)) ∧
(∀c. P c ⇒ ∀l. P (canonical.Cons_varlist l c)) ⇒ ∀c. P c
⊦ (∀f. quote.varmap_size f quote.Empty_vm = 0) ∧
∀f a0 a1 a2.
quote.varmap_size f (quote.Node_vm a0 a1 a2) =
1 + (f a0 + (quote.varmap_size f a1 + quote.varmap_size f a2))
⊦ ∀r.
(∀vm c. ringNorm.r_interp_m r vm c [] = c) ∧
∀vm c x t.
ringNorm.r_interp_m r vm c (x :: t) =
ring.ring_RM r c (ringNorm.r_ivl_aux r vm x t)
⊦ ∀s a0 a f0 f.
semi_ring.semi_ring_SR0_fupd (const a0)
(semi_ring.semi_ring_SR1_fupd (const a)
(semi_ring.semi_ring_SRP_fupd (const f0)
(semi_ring.semi_ring_SRM_fupd (const f) s))) =
semi_ring.semi_ring_SR0_fupd (const a0)
(semi_ring.semi_ring_SR1_fupd (const a)
(semi_ring.semi_ring_SRP_fupd (const f0)
(semi_ring.semi_ring_SRM_fupd (const f) bool.ARB)))
⊦ ∀r1 r2.
r1 = r2 ⇔
ring.ring_R0 r1 = ring.ring_R0 r2 ∧ ring.ring_R1 r1 = ring.ring_R1 r2 ∧
ring.ring_RP r1 = ring.ring_RP r2 ∧ ring.ring_RM r1 = ring.ring_RM r2 ∧
ring.ring_RN r1 = ring.ring_RN r2
⊦ (∀sr vm c. canonical.interp_m sr vm c [] = c) ∧
∀sr vm c x t.
canonical.interp_m sr vm c (x :: t) =
semi_ring.semi_ring_SRM sr c (canonical.ivl_aux sr vm x t)
⊦ (∀lt eq gt. prelim.compare prelim.LESS lt eq gt = lt) ∧
(∀lt eq gt. prelim.compare prelim.EQUAL lt eq gt = eq) ∧
∀lt eq gt. prelim.compare prelim.GREATER lt eq gt = gt
⊦ (∀v0 v1 v2. prelim.ordering_CASE prelim.LESS v0 v1 v2 = v0) ∧
(∀v0 v1 v2. prelim.ordering_CASE prelim.EQUAL v0 v1 v2 = v1) ∧
∀v0 v1 v2. prelim.ordering_CASE prelim.GREATER v0 v1 v2 = v2
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0'.
∀'semi_ring'.
(∀a0'.
(∃a0 a1 a2 a3.
a0' =
(let a0 ← a0 in
λa1 a2 a3.
ind_type.CONSTR 0 (a0, a1, a2, a3)
(λn. ind_type.BOTTOM)) a1 a2 a3) ⇒ 'semi_ring' a0') ⇒
'semi_ring' a0') rep
⊦ ∀x.
(∃i. x = ringNorm.Pvar i) ∨ (∃a. x = ringNorm.Pconst a) ∨
(∃p p0. x = ringNorm.Pplus p p0) ∨ (∃p p0. x = ringNorm.Pmult p p0) ∨
∃p. x = ringNorm.Popp p
⊦ ∀r.
(∀vm x. ringNorm.r_ivl_aux r vm x [] = quote.varmap_find x vm) ∧
∀vm x x' t'.
ringNorm.r_ivl_aux r vm x (x' :: t') =
ring.ring_RM r (quote.varmap_find x vm)
(ringNorm.r_ivl_aux r vm x' t')
⊦ ∀a0 a1 a2 a3 a0' a1' a2' a3'.
semi_ring.recordtype.semi_ring a0 a1 a2 a3 =
semi_ring.recordtype.semi_ring a0' a1' a2' a3' ⇔
a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3'
⊦ (∀a2 a1 a0. ¬(canonical.Nil_monom = canonical.Cons_monom a0 a1 a2)) ∧
(∀a1 a0. ¬(canonical.Nil_monom = canonical.Cons_varlist a0 a1)) ∧
∀a2 a1' a1 a0' a0.
¬(canonical.Cons_monom a0 a1 a2 = canonical.Cons_varlist a0' a1')
⊦ (∀sr vm x. canonical.ivl_aux sr vm x [] = quote.varmap_find x vm) ∧
∀sr vm x x' t'.
canonical.ivl_aux sr vm x (x' :: t') =
semi_ring.semi_ring_SRM sr (quote.varmap_find x vm)
(canonical.ivl_aux sr vm x' t')
⊦ ∀f0 f1 f2.
∃fn.
fn canonical.Nil_monom = f0 ∧
(∀a0 a1 a2.
fn (canonical.Cons_monom a0 a1 a2) = f1 a0 a1 a2 (fn a2)) ∧
∀a0 a1. fn (canonical.Cons_varlist a0 a1) = f2 a0 a1 (fn a1)
⊦ ∀M M' f.
M = M' ∧
(∀a0 a1 a2 a3.
M' = semi_ring.recordtype.semi_ring a0 a1 a2 a3 ⇒
f a0 a1 a2 a3 = f' a0 a1 a2 a3) ⇒
semi_ring.semi_ring_CASE M f = semi_ring.semi_ring_CASE M' f'
⊦ ∀r a0 a f1 f0 f.
ring.ring_R0_fupd (const a0)
(ring.ring_R1_fupd (const a)
(ring.ring_RP_fupd (const f1)
(ring.ring_RM_fupd (const f0)
(ring.ring_RN_fupd (const f) r)))) =
ring.ring_R0_fupd (const a0)
(ring.ring_R1_fupd (const a)
(ring.ring_RP_fupd (const f1)
(ring.ring_RM_fupd (const f0)
(ring.ring_RN_fupd (const f) bool.ARB))))
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0'.
∀'ring'.
(∀a0'.
(∃a0 a1 a2 a3 a4.
a0' =
(let a0 ← a0 in
λa1 a2 a3 a4.
ind_type.CONSTR 0 (a0, a1, a2, a3, a4)
(λn. ind_type.BOTTOM)) a1 a2 a3 a4) ⇒ 'ring' a0') ⇒
'ring' a0') rep
⊦ (∀a f f1 v. quote.index_CASE (quote.Left_idx a) f f1 v = f a) ∧
(∀a f f1 v. quote.index_CASE (quote.Right_idx a) f f1 v = f1 a) ∧
∀f f1 v. quote.index_CASE quote.End_idx f f1 v = v
⊦ ∀P.
(∀i. P (canonical.SPvar i)) ∧ (∀a. P (canonical.SPconst a)) ∧
(∀s s0. P s ∧ P s0 ⇒ P (canonical.SPplus s s0)) ∧
(∀s s0. P s ∧ P s0 ⇒ P (canonical.SPmult s s0)) ⇒ ∀s. P s
⊦ ∀M M' f.
M = M' ∧
(∀a0 a1 a2 a3 a4.
M' = ring.recordtype.ring a0 a1 a2 a3 a4 ⇒
f a0 a1 a2 a3 a4 = f' a0 a1 a2 a3 a4) ⇒
ring.ring_CASE M f = ring.ring_CASE M' f'
⊦ ∀M M' v0 v1 v2.
M = M' ∧ (M' = prelim.LESS ⇒ v0 = v0') ∧
(M' = prelim.EQUAL ⇒ v1 = v1') ∧ (M' = prelim.GREATER ⇒ v2 = v2') ⇒
prelim.ordering_CASE M v0 v1 v2 = prelim.ordering_CASE M' v0' v1' v2'
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0'.
∀'varmap'.
(∀a0'.
a0' = ind_type.CONSTR 0 bool.ARB (λn. ind_type.BOTTOM) ∨
(∃a0 a1 a2.
a0' =
(let a0 ← a0 in
λa1 a2.
ind_type.CONSTR (suc 0) a0
(ind_type.FCONS a1
(ind_type.FCONS a2 (λn. ind_type.BOTTOM)))) a1
a2 ∧ 'varmap' a1 ∧ 'varmap' a2) ⇒ 'varmap' a0') ⇒
'varmap' a0') rep
⊦ ∀a0 a1 a2 a3 a4 a0' a1' a2' a3' a4'.
ring.recordtype.ring a0 a1 a2 a3 a4 =
ring.recordtype.ring a0' a1' a2' a3' a4' ⇔
a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3' ∧ a4 = a4'
⊦ ∀M M' v f.
M = M' ∧ (M' = quote.Empty_vm ⇒ v = v') ∧
(∀a0 a1 a2. M' = quote.Node_vm a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
quote.varmap_CASE M v f = quote.varmap_CASE M' v' f'
⊦ (∀a0 a1 a2 a0' a1' a2'.
canonical.Cons_monom a0 a1 a2 = canonical.Cons_monom a0' a1' a2' ⇔
a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
∀a0 a1 a0' a1'.
canonical.Cons_varlist a0 a1 = canonical.Cons_varlist a0' a1' ⇔
a0 = a0' ∧ a1 = a1'
⊦ ∀P.
(∀i. P (ringNorm.Pvar i)) ∧ (∀a. P (ringNorm.Pconst a)) ∧
(∀p p0. P p ∧ P p0 ⇒ P (ringNorm.Pplus p p0)) ∧
(∀p p0. P p ∧ P p0 ⇒ P (ringNorm.Pmult p p0)) ∧
(∀p. P p ⇒ P (ringNorm.Popp p)) ⇒ ∀p. P p
⊦ ∀r.
(∀c0 c l t.
ringNorm.r_canonical_sum_scalar r c0 (canonical.Cons_monom c l t) =
canonical.Cons_monom (ring.ring_RM r c0 c) l
(ringNorm.r_canonical_sum_scalar r c0 t)) ∧
(∀c0 l t.
ringNorm.r_canonical_sum_scalar r c0 (canonical.Cons_varlist l t) =
canonical.Cons_monom c0 l
(ringNorm.r_canonical_sum_scalar r c0 t)) ∧
∀c0.
ringNorm.r_canonical_sum_scalar r c0 canonical.Nil_monom =
canonical.Nil_monom
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0.
∀'index'.
(∀a0.
(∃a.
a0 =
(let a ← a in
ind_type.CONSTR 0 bool.ARB
(ind_type.FCONS a (λn. ind_type.BOTTOM))) ∧
'index' a) ∨
(∃a.
a0 =
(let a ← a in
ind_type.CONSTR (suc 0) bool.ARB
(ind_type.FCONS a (λn. ind_type.BOTTOM))) ∧
'index' a) ∨
a0 =
ind_type.CONSTR (suc (suc 0)) bool.ARB
(λn. ind_type.BOTTOM) ⇒ 'index' a0) ⇒ 'index' a0) rep
⊦ (∀v f f1. canonical.canonical_sum_CASE canonical.Nil_monom v f f1 = v) ∧
(∀a0 a1 a2 v f f1.
canonical.canonical_sum_CASE (canonical.Cons_monom a0 a1 a2) v f f1 =
f a0 a1 a2) ∧
∀a0 a1 v f f1.
canonical.canonical_sum_CASE (canonical.Cons_varlist a0 a1) v f f1 =
f1 a0 a1
⊦ ∀r.
(∀vm. ringNorm.r_interp_cs r vm canonical.Nil_monom = ring.ring_R0 r) ∧
(∀vm l t.
ringNorm.r_interp_cs r vm (canonical.Cons_varlist l t) =
ringNorm.r_ics_aux r vm (ringNorm.r_interp_vl r vm l) t) ∧
∀vm c l t.
ringNorm.r_interp_cs r vm (canonical.Cons_monom c l t) =
ringNorm.r_ics_aux r vm (ringNorm.r_interp_m r vm c l) t
⊦ ∀a01 a1 f01 f1 a02 a2 f02 f2.
semi_ring.semi_ring_SR0_fupd (const a01)
(semi_ring.semi_ring_SR1_fupd (const a1)
(semi_ring.semi_ring_SRP_fupd (const f01)
(semi_ring.semi_ring_SRM_fupd (const f1) bool.ARB))) =
semi_ring.semi_ring_SR0_fupd (const a02)
(semi_ring.semi_ring_SR1_fupd (const a2)
(semi_ring.semi_ring_SRP_fupd (const f02)
(semi_ring.semi_ring_SRM_fupd (const f2) bool.ARB))) ⇔
a01 = a02 ∧ a1 = a2 ∧ f01 = f02 ∧ f1 = f2
⊦ (∀f. canonical.canonical_sum_size f canonical.Nil_monom = 0) ∧
(∀f a0 a1 a2.
canonical.canonical_sum_size f (canonical.Cons_monom a0 a1 a2) =
1 +
(f a0 +
(list.list_size quote.index_size a1 +
canonical.canonical_sum_size f a2))) ∧
∀f a0 a1.
canonical.canonical_sum_size f (canonical.Cons_varlist a0 a1) =
1 +
(list.list_size quote.index_size a0 +
canonical.canonical_sum_size f a1)
⊦ ∀M M' f f1 v.
M = M' ∧ (∀a. M' = quote.Left_idx a ⇒ f a = f' a) ∧
(∀a. M' = quote.Right_idx a ⇒ f1 a = f1' a) ∧
(M' = quote.End_idx ⇒ v = v') ⇒
quote.index_CASE M f f1 v = quote.index_CASE M' f' f1' v'
⊦ ∀f0 f1 f2 f3.
∃fn.
(∀a. fn (canonical.SPvar a) = f0 a) ∧
(∀a. fn (canonical.SPconst a) = f1 a) ∧
(∀a0 a1. fn (canonical.SPplus a0 a1) = f2 a0 a1 (fn a0) (fn a1)) ∧
∀a0 a1. fn (canonical.SPmult a0 a1) = f3 a0 a1 (fn a0) (fn a1)
⊦ ∀P.
(∀sr l1 c2 l2 t2.
P sr l1 t2 ⇒ P sr l1 (canonical.Cons_monom c2 l2 t2)) ∧
(∀sr l1 l2 t2. P sr l1 t2 ⇒ P sr l1 (canonical.Cons_varlist l2 t2)) ∧
(∀sr l1. P sr l1 canonical.Nil_monom) ⇒ ∀v v1 v2. P v v1 v2
⊦ (∀sr c0 c l t.
canonical.canonical_sum_scalar sr c0 (canonical.Cons_monom c l t) =
canonical.Cons_monom (semi_ring.semi_ring_SRM sr c0 c) l
(canonical.canonical_sum_scalar sr c0 t)) ∧
(∀sr c0 l t.
canonical.canonical_sum_scalar sr c0 (canonical.Cons_varlist l t) =
canonical.Cons_monom c0 l (canonical.canonical_sum_scalar sr c0 t)) ∧
∀sr c0.
canonical.canonical_sum_scalar sr c0 canonical.Nil_monom =
canonical.Nil_monom
⊦ ∀r.
(∀c1 l1 t1 s2.
ringNorm.r_canonical_sum_prod r (canonical.Cons_monom c1 l1 t1) s2 =
ringNorm.r_canonical_sum_merge r
(ringNorm.r_canonical_sum_scalar3 r c1 l1 s2)
(ringNorm.r_canonical_sum_prod r t1 s2)) ∧
(∀l1 t1 s2.
ringNorm.r_canonical_sum_prod r (canonical.Cons_varlist l1 t1) s2 =
ringNorm.r_canonical_sum_merge r
(ringNorm.r_canonical_sum_scalar2 r l1 s2)
(ringNorm.r_canonical_sum_prod r t1 s2)) ∧
∀s2.
ringNorm.r_canonical_sum_prod r canonical.Nil_monom s2 =
canonical.Nil_monom
⊦ ∀r.
(∀l0 c l t.
ringNorm.r_canonical_sum_scalar2 r l0 (canonical.Cons_monom c l t) =
ringNorm.r_monom_insert r c (prelim.list_merge quote.index_lt l0 l)
(ringNorm.r_canonical_sum_scalar2 r l0 t)) ∧
(∀l0 l t.
ringNorm.r_canonical_sum_scalar2 r l0 (canonical.Cons_varlist l t) =
ringNorm.r_varlist_insert r (prelim.list_merge quote.index_lt l0 l)
(ringNorm.r_canonical_sum_scalar2 r l0 t)) ∧
∀l0.
ringNorm.r_canonical_sum_scalar2 r l0 canonical.Nil_monom =
canonical.Nil_monom
⊦ (∀sr vm.
canonical.interp_cs sr vm canonical.Nil_monom =
semi_ring.semi_ring_SR0 sr) ∧
(∀sr vm l t.
canonical.interp_cs sr vm (canonical.Cons_varlist l t) =
canonical.ics_aux sr vm (canonical.interp_vl sr vm l) t) ∧
∀sr vm c l t.
canonical.interp_cs sr vm (canonical.Cons_monom c l t) =
canonical.ics_aux sr vm (canonical.interp_m sr vm c l) t
⊦ (∀x v2 v1. quote.varmap_find quote.End_idx (quote.Node_vm x v1 v2) = x) ∧
(∀x v2 v1 i1.
quote.varmap_find (quote.Right_idx i1) (quote.Node_vm x v1 v2) =
quote.varmap_find i1 v2) ∧
(∀x v2 v1 i1.
quote.varmap_find (quote.Left_idx i1) (quote.Node_vm x v1 v2) =
quote.varmap_find i1 v1) ∧
∀i. quote.varmap_find i quote.Empty_vm = select x. ⊤
⊦ ∀r.
(∀c l t.
ringNorm.r_canonical_sum_simplify r (canonical.Cons_monom c l t) =
if c = ring.ring_R0 r then ringNorm.r_canonical_sum_simplify r t
else if c = ring.ring_R1 r then
canonical.Cons_varlist l (ringNorm.r_canonical_sum_simplify r t)
else
canonical.Cons_monom c l
(ringNorm.r_canonical_sum_simplify r t)) ∧
(∀l t.
ringNorm.r_canonical_sum_simplify r (canonical.Cons_varlist l t) =
canonical.Cons_varlist l (ringNorm.r_canonical_sum_simplify r t)) ∧
ringNorm.r_canonical_sum_simplify r canonical.Nil_monom =
canonical.Nil_monom
⊦ (∀a a0 f f0.
semi_ring.semi_ring_SR0 (semi_ring.recordtype.semi_ring a a0 f f0) =
a) ∧
(∀a a0 f f0.
semi_ring.semi_ring_SR1 (semi_ring.recordtype.semi_ring a a0 f f0) =
a0) ∧
(∀a a0 f f0.
semi_ring.semi_ring_SRP (semi_ring.recordtype.semi_ring a a0 f f0) =
f) ∧
∀a a0 f f0.
semi_ring.semi_ring_SRM (semi_ring.recordtype.semi_ring a a0 f f0) = f0
⊦ ∀r.
(∀i.
ringNorm.r_spolynom_normalize r (canonical.SPvar i) =
canonical.Cons_varlist (i :: []) canonical.Nil_monom) ∧
(∀c.
ringNorm.r_spolynom_normalize r (canonical.SPconst c) =
canonical.Cons_monom c [] canonical.Nil_monom) ∧
(∀l r'.
ringNorm.r_spolynom_normalize r (canonical.SPplus l r') =
ringNorm.r_canonical_sum_merge r (ringNorm.r_spolynom_normalize r l)
(ringNorm.r_spolynom_normalize r r')) ∧
∀l r'.
ringNorm.r_spolynom_normalize r (canonical.SPmult l r') =
ringNorm.r_canonical_sum_prod r (ringNorm.r_spolynom_normalize r l)
(ringNorm.r_spolynom_normalize r r')
⊦ ∀P.
(∀x v1 v2. P quote.End_idx (quote.Node_vm x v1 v2)) ∧
(∀i1 x v1 v2.
P i1 v2 ⇒ P (quote.Right_idx i1) (quote.Node_vm x v1 v2)) ∧
(∀i1 x v1 v2.
P i1 v1 ⇒ P (quote.Left_idx i1) (quote.Node_vm x v1 v2)) ∧
(∀i. P i quote.Empty_vm) ⇒ ∀v v1. P v v1
⊦ (∀sr c1 l1 t1 s2.
canonical.canonical_sum_prod sr (canonical.Cons_monom c1 l1 t1) s2 =
canonical.canonical_sum_merge sr
(canonical.canonical_sum_scalar3 sr c1 l1 s2)
(canonical.canonical_sum_prod sr t1 s2)) ∧
(∀sr l1 t1 s2.
canonical.canonical_sum_prod sr (canonical.Cons_varlist l1 t1) s2 =
canonical.canonical_sum_merge sr
(canonical.canonical_sum_scalar2 sr l1 s2)
(canonical.canonical_sum_prod sr t1 s2)) ∧
∀sr s2.
canonical.canonical_sum_prod sr canonical.Nil_monom s2 =
canonical.Nil_monom
⊦ (∀sr l0 c l t.
canonical.canonical_sum_scalar2 sr l0 (canonical.Cons_monom c l t) =
canonical.monom_insert sr c (prelim.list_merge quote.index_lt l0 l)
(canonical.canonical_sum_scalar2 sr l0 t)) ∧
(∀sr l0 l t.
canonical.canonical_sum_scalar2 sr l0 (canonical.Cons_varlist l t) =
canonical.varlist_insert sr (prelim.list_merge quote.index_lt l0 l)
(canonical.canonical_sum_scalar2 sr l0 t)) ∧
∀sr l0.
canonical.canonical_sum_scalar2 sr l0 canonical.Nil_monom =
canonical.Nil_monom
⊦ ∀P.
(∀cmp. P cmp [] []) ∧ (∀cmp v8 v9. P cmp [] (v8 :: v9)) ∧
(∀cmp v4 v5. P cmp (v4 :: v5) []) ∧
(∀cmp x l1 y l2. P cmp l1 l2 ⇒ P cmp (x :: l1) (y :: l2)) ⇒
∀v v1 v2. P v v1 v2
⊦ (∀sr c l t.
canonical.canonical_sum_simplify sr (canonical.Cons_monom c l t) =
if c = semi_ring.semi_ring_SR0 sr then
canonical.canonical_sum_simplify sr t
else if c = semi_ring.semi_ring_SR1 sr then
canonical.Cons_varlist l (canonical.canonical_sum_simplify sr t)
else
canonical.Cons_monom c l (canonical.canonical_sum_simplify sr t)) ∧
(∀sr l t.
canonical.canonical_sum_simplify sr (canonical.Cons_varlist l t) =
canonical.Cons_varlist l (canonical.canonical_sum_simplify sr t)) ∧
∀sr.
canonical.canonical_sum_simplify sr canonical.Nil_monom =
canonical.Nil_monom
⊦ (∀cmp. prelim.list_compare cmp [] [] = prelim.EQUAL) ∧
(∀v9 v8 cmp. prelim.list_compare cmp [] (v8 :: v9) = prelim.LESS) ∧
(∀v5 v4 cmp. prelim.list_compare cmp (v4 :: v5) [] = prelim.GREATER) ∧
∀y x l2 l1 cmp.
prelim.list_compare cmp (x :: l1) (y :: l2) =
prelim.compare (cmp x y) prelim.LESS (prelim.list_compare cmp l1 l2)
prelim.GREATER
⊦ (∀l1 a_lt. prelim.list_merge a_lt l1 [] = l1) ∧
(∀v5 v4 a_lt. prelim.list_merge a_lt [] (v4 :: v5) = v4 :: v5) ∧
∀y x l2 l1 a_lt.
prelim.list_merge a_lt (x :: l1) (y :: l2) =
if a_lt x y then x :: prelim.list_merge a_lt l1 (y :: l2)
else y :: prelim.list_merge a_lt (x :: l1) l2
⊦ prelim.list_compare_tupled =
relation.WFREC
(select R.
wellFounded R ∧
∀y x l2 l1 cmp. R (cmp, l1, l2) (cmp, x :: l1, y :: l2))
(λlist_compare_tupled a.
pair.pair_CASE a
(λcmp v1.
pair.pair_CASE v1
(λv2 v3.
list.list_CASE v2
(list.list_CASE v3 (id prelim.EQUAL)
(λv10 v11. id prelim.LESS))
(λx l1.
list.list_CASE v3 (id prelim.GREATER)
(λy l2.
id
(prelim.compare (cmp x y) prelim.LESS
(list_compare_tupled (cmp, l1, l2))
prelim.GREATER))))))
⊦ (∀sr i.
canonical.spolynom_normalize sr (canonical.SPvar i) =
canonical.Cons_varlist (i :: []) canonical.Nil_monom) ∧
(∀sr c.
canonical.spolynom_normalize sr (canonical.SPconst c) =
canonical.Cons_monom c [] canonical.Nil_monom) ∧
(∀sr l r.
canonical.spolynom_normalize sr (canonical.SPplus l r) =
canonical.canonical_sum_merge sr (canonical.spolynom_normalize sr l)
(canonical.spolynom_normalize sr r)) ∧
∀sr l r.
canonical.spolynom_normalize sr (canonical.SPmult l r) =
canonical.canonical_sum_prod sr (canonical.spolynom_normalize sr l)
(canonical.spolynom_normalize sr r)
⊦ (∀s g f.
semi_ring.semi_ring_SR0_fupd f (semi_ring.semi_ring_SR0_fupd g s) =
semi_ring.semi_ring_SR0_fupd (f ∘ g) s) ∧
(∀s g f.
semi_ring.semi_ring_SR1_fupd f (semi_ring.semi_ring_SR1_fupd g s) =
semi_ring.semi_ring_SR1_fupd (f ∘ g) s) ∧
(∀s g f.
semi_ring.semi_ring_SRP_fupd f (semi_ring.semi_ring_SRP_fupd g s) =
semi_ring.semi_ring_SRP_fupd (f ∘ g) s) ∧
∀s g f.
semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SRM_fupd g s) =
semi_ring.semi_ring_SRM_fupd (f ∘ g) s
⊦ ∀r.
(∀vm a. ringNorm.r_ics_aux r vm a canonical.Nil_monom = a) ∧
(∀vm a l t.
ringNorm.r_ics_aux r vm a (canonical.Cons_varlist l t) =
ring.ring_RP r a
(ringNorm.r_ics_aux r vm (ringNorm.r_interp_vl r vm l) t)) ∧
∀vm a c l t.
ringNorm.r_ics_aux r vm a (canonical.Cons_monom c l t) =
ring.ring_RP r a
(ringNorm.r_ics_aux r vm (ringNorm.r_interp_m r vm c l) t)
⊦ ∀f0 f1 f2 f3 f4.
∃fn.
(∀a. fn (ringNorm.Pvar a) = f0 a) ∧
(∀a. fn (ringNorm.Pconst a) = f1 a) ∧
(∀a0 a1. fn (ringNorm.Pplus a0 a1) = f2 a0 a1 (fn a0) (fn a1)) ∧
(∀a0 a1. fn (ringNorm.Pmult a0 a1) = f3 a0 a1 (fn a0) (fn a1)) ∧
∀a. fn (ringNorm.Popp a) = f4 a (fn a)
⊦ ∀a01 a1 f11 f01 f1 a02 a2 f12 f02 f2.
ring.ring_R0_fupd (const a01)
(ring.ring_R1_fupd (const a1)
(ring.ring_RP_fupd (const f11)
(ring.ring_RM_fupd (const f01)
(ring.ring_RN_fupd (const f1) bool.ARB)))) =
ring.ring_R0_fupd (const a02)
(ring.ring_R1_fupd (const a2)
(ring.ring_RP_fupd (const f12)
(ring.ring_RM_fupd (const f02)
(ring.ring_RN_fupd (const f2) bool.ARB)))) ⇔
a01 = a02 ∧ a1 = a2 ∧ f11 = f12 ∧ f01 = f02 ∧ f1 = f2
⊦ ∀P.
(∀sr c1 l1 c2 l2 t2.
P sr c1 l1 t2 ⇒ P sr c1 l1 (canonical.Cons_monom c2 l2 t2)) ∧
(∀sr c1 l1 l2 t2.
P sr c1 l1 t2 ⇒ P sr c1 l1 (canonical.Cons_varlist l2 t2)) ∧
(∀sr c1 l1. P sr c1 l1 canonical.Nil_monom) ⇒ ∀v v1 v2 v3. P v v1 v2 v3
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0'.
∀'canonical_sum'.
(∀a0'.
a0' =
ind_type.CONSTR 0 (bool.ARB, bool.ARB)
(λn. ind_type.BOTTOM) ∨
(∃a0 a1 a2.
a0' =
(let a0 ← a0 in
λa1 a2.
ind_type.CONSTR (suc 0) (a0, a1)
(ind_type.FCONS a2 (λn. ind_type.BOTTOM))) a1 a2 ∧
'canonical_sum' a2) ∨
(∃a0 a1.
a0' =
(let a0 ← a0 in
λa1.
ind_type.CONSTR (suc (suc 0)) (bool.ARB, a0)
(ind_type.FCONS a1 (λn. ind_type.BOTTOM))) a1 ∧
'canonical_sum' a1) ⇒ 'canonical_sum' a0') ⇒
'canonical_sum' a0') rep
⊦ quote.varmap_find_tupled =
relation.WFREC
(select R.
wellFounded R ∧
(∀v1 x v2 i1.
R (i1, v2) (quote.Right_idx i1, quote.Node_vm x v1 v2)) ∧
∀v2 x v1 i1. R (i1, v1) (quote.Left_idx i1, quote.Node_vm x v1 v2))
(λvarmap_find_tupled a.
pair.pair_CASE a
(λv3 v4.
quote.varmap_CASE v4 (id (select x. ⊤))
(λx v1 v2.
quote.index_CASE v3
(λi1'. id (varmap_find_tupled (i1', v1)))
(λi1. id (varmap_find_tupled (i1, v2))) (id x))))
⊦ ∀M M' v f f1.
M = M' ∧ (M' = canonical.Nil_monom ⇒ v = v') ∧
(∀a0 a1 a2.
M' = canonical.Cons_monom a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ∧
(∀a0 a1. M' = canonical.Cons_varlist a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ⇒
canonical.canonical_sum_CASE M v f f1 =
canonical.canonical_sum_CASE M' v' f' f1'
⊦ ∀P.
(∀a_lt l1. P a_lt l1 []) ∧ (∀a_lt v4 v5. P a_lt [] (v4 :: v5)) ∧
(∀a_lt x l1 y l2.
(¬a_lt x y ⇒ P a_lt (x :: l1) l2) ∧
(a_lt x y ⇒ P a_lt l1 (y :: l2)) ⇒ P a_lt (x :: l1) (y :: l2)) ⇒
∀v v1 v2. P v v1 v2
⊦ (∀a a'. canonical.SPvar a = canonical.SPvar a' ⇔ a = a') ∧
(∀a a'. canonical.SPconst a = canonical.SPconst a' ⇔ a = a') ∧
(∀a0 a1 a0' a1'.
canonical.SPplus a0 a1 = canonical.SPplus a0' a1' ⇔
a0 = a0' ∧ a1 = a1') ∧
∀a0 a1 a0' a1'.
canonical.SPmult a0 a1 = canonical.SPmult a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
⊦ ∀r.
(∀vm c. ringNorm.r_interp_sp r vm (canonical.SPconst c) = c) ∧
(∀vm i.
ringNorm.r_interp_sp r vm (canonical.SPvar i) =
quote.varmap_find i vm) ∧
(∀vm p1 p2.
ringNorm.r_interp_sp r vm (canonical.SPplus p1 p2) =
ring.ring_RP r (ringNorm.r_interp_sp r vm p1)
(ringNorm.r_interp_sp r vm p2)) ∧
∀vm p1 p2.
ringNorm.r_interp_sp r vm (canonical.SPmult p1 p2) =
ring.ring_RM r (ringNorm.r_interp_sp r vm p1)
(ringNorm.r_interp_sp r vm p2)
⊦ (∀sr vm a. canonical.ics_aux sr vm a canonical.Nil_monom = a) ∧
(∀sr vm a l t.
canonical.ics_aux sr vm a (canonical.Cons_varlist l t) =
semi_ring.semi_ring_SRP sr a
(canonical.ics_aux sr vm (canonical.interp_vl sr vm l) t)) ∧
∀sr vm a c l t.
canonical.ics_aux sr vm a (canonical.Cons_monom c l t) =
semi_ring.semi_ring_SRP sr a
(canonical.ics_aux sr vm (canonical.interp_m sr vm c l) t)
⊦ (∀f a.
canonical.spolynom_size f (canonical.SPvar a) =
1 + quote.index_size a) ∧
(∀f a. canonical.spolynom_size f (canonical.SPconst a) = 1 + f a) ∧
(∀f a0 a1.
canonical.spolynom_size f (canonical.SPplus a0 a1) =
1 + (canonical.spolynom_size f a0 + canonical.spolynom_size f a1)) ∧
∀f a0 a1.
canonical.spolynom_size f (canonical.SPmult a0 a1) =
1 + (canonical.spolynom_size f a0 + canonical.spolynom_size f a1)
⊦ ∀r.
(∀c0 l0 c l t.
ringNorm.r_canonical_sum_scalar3 r c0 l0
(canonical.Cons_monom c l t) =
ringNorm.r_monom_insert r (ring.ring_RM r c0 c)
(prelim.list_merge quote.index_lt l0 l)
(ringNorm.r_canonical_sum_scalar3 r c0 l0 t)) ∧
(∀c0 l0 l t.
ringNorm.r_canonical_sum_scalar3 r c0 l0
(canonical.Cons_varlist l t) =
ringNorm.r_monom_insert r c0 (prelim.list_merge quote.index_lt l0 l)
(ringNorm.r_canonical_sum_scalar3 r c0 l0 t)) ∧
∀c0 l0.
ringNorm.r_canonical_sum_scalar3 r c0 l0 canonical.Nil_monom =
canonical.Nil_monom
⊦ (∀a' a. ¬(canonical.SPvar a = canonical.SPconst a')) ∧
(∀a1 a0 a. ¬(canonical.SPvar a = canonical.SPplus a0 a1)) ∧
(∀a1 a0 a. ¬(canonical.SPvar a = canonical.SPmult a0 a1)) ∧
(∀a1 a0 a. ¬(canonical.SPconst a = canonical.SPplus a0 a1)) ∧
(∀a1 a0 a. ¬(canonical.SPconst a = canonical.SPmult a0 a1)) ∧
∀a1' a1 a0' a0. ¬(canonical.SPplus a0 a1 = canonical.SPmult a0' a1')
⊦ (∀sr vm c. canonical.interp_sp sr vm (canonical.SPconst c) = c) ∧
(∀sr vm i.
canonical.interp_sp sr vm (canonical.SPvar i) =
quote.varmap_find i vm) ∧
(∀sr vm p1 p2.
canonical.interp_sp sr vm (canonical.SPplus p1 p2) =
semi_ring.semi_ring_SRP sr (canonical.interp_sp sr vm p1)
(canonical.interp_sp sr vm p2)) ∧
∀sr vm p1 p2.
canonical.interp_sp sr vm (canonical.SPmult p1 p2) =
semi_ring.semi_ring_SRM sr (canonical.interp_sp sr vm p1)
(canonical.interp_sp sr vm p2)
⊦ (∀sr c0 l0 c l t.
canonical.canonical_sum_scalar3 sr c0 l0
(canonical.Cons_monom c l t) =
canonical.monom_insert sr (semi_ring.semi_ring_SRM sr c0 c)
(prelim.list_merge quote.index_lt l0 l)
(canonical.canonical_sum_scalar3 sr c0 l0 t)) ∧
(∀sr c0 l0 l t.
canonical.canonical_sum_scalar3 sr c0 l0
(canonical.Cons_varlist l t) =
canonical.monom_insert sr c0 (prelim.list_merge quote.index_lt l0 l)
(canonical.canonical_sum_scalar3 sr c0 l0 t)) ∧
∀sr c0 l0.
canonical.canonical_sum_scalar3 sr c0 l0 canonical.Nil_monom =
canonical.Nil_monom
⊦ (∀a f f1 f2 f3.
canonical.spolynom_CASE (canonical.SPvar a) f f1 f2 f3 = f a) ∧
(∀a f f1 f2 f3.
canonical.spolynom_CASE (canonical.SPconst a) f f1 f2 f3 = f1 a) ∧
(∀a0 a1 f f1 f2 f3.
canonical.spolynom_CASE (canonical.SPplus a0 a1) f f1 f2 f3 =
f2 a0 a1) ∧
∀a0 a1 f f1 f2 f3.
canonical.spolynom_CASE (canonical.SPmult a0 a1) f f1 f2 f3 = f3 a0 a1
⊦ ∀P.
P quote.End_idx quote.End_idx ∧
(∀v10. P quote.End_idx (quote.Left_idx v10)) ∧
(∀v11. P quote.End_idx (quote.Right_idx v11)) ∧
(∀v2. P (quote.Left_idx v2) quote.End_idx) ∧
(∀v3. P (quote.Right_idx v3) quote.End_idx) ∧
(∀n' m'. P n' m' ⇒ P (quote.Left_idx n') (quote.Left_idx m')) ∧
(∀n' m'. P (quote.Left_idx n') (quote.Right_idx m')) ∧
(∀n' m'. P n' m' ⇒ P (quote.Right_idx n') (quote.Right_idx m')) ∧
(∀n' m'. P (quote.Right_idx n') (quote.Left_idx m')) ⇒ ∀v v1. P v v1
⊦ (∀r g f.
ring.ring_R0_fupd f (ring.ring_R0_fupd g r) =
ring.ring_R0_fupd (f ∘ g) r) ∧
(∀r g f.
ring.ring_R1_fupd f (ring.ring_R1_fupd g r) =
ring.ring_R1_fupd (f ∘ g) r) ∧
(∀r g f.
ring.ring_RP_fupd f (ring.ring_RP_fupd g r) =
ring.ring_RP_fupd (f ∘ g) r) ∧
(∀r g f.
ring.ring_RM_fupd f (ring.ring_RM_fupd g r) =
ring.ring_RM_fupd (f ∘ g) r) ∧
∀r g f.
ring.ring_RN_fupd f (ring.ring_RN_fupd g r) =
ring.ring_RN_fupd (f ∘ g) r
⊦ (∀a a'. ringNorm.Pvar a = ringNorm.Pvar a' ⇔ a = a') ∧
(∀a a'. ringNorm.Pconst a = ringNorm.Pconst a' ⇔ a = a') ∧
(∀a0 a1 a0' a1'.
ringNorm.Pplus a0 a1 = ringNorm.Pplus a0' a1' ⇔ a0 = a0' ∧ a1 = a1') ∧
(∀a0 a1 a0' a1'.
ringNorm.Pmult a0 a1 = ringNorm.Pmult a0' a1' ⇔ a0 = a0' ∧ a1 = a1') ∧
∀a a'. ringNorm.Popp a = ringNorm.Popp a' ⇔ a = a'
⊦ (∀r i.
ringNorm.polynom_normalize r (ringNorm.Pvar i) =
canonical.Cons_varlist (i :: []) canonical.Nil_monom) ∧
(∀r c.
ringNorm.polynom_normalize r (ringNorm.Pconst c) =
canonical.Cons_monom c [] canonical.Nil_monom) ∧
(∀r pl pr.
ringNorm.polynom_normalize r (ringNorm.Pplus pl pr) =
ringNorm.r_canonical_sum_merge r (ringNorm.polynom_normalize r pl)
(ringNorm.polynom_normalize r pr)) ∧
(∀r pl pr.
ringNorm.polynom_normalize r (ringNorm.Pmult pl pr) =
ringNorm.r_canonical_sum_prod r (ringNorm.polynom_normalize r pl)
(ringNorm.polynom_normalize r pr)) ∧
∀r p.
ringNorm.polynom_normalize r (ringNorm.Popp p) =
ringNorm.r_canonical_sum_scalar3 r (ring.ring_RN r (ring.ring_R1 r)) []
(ringNorm.polynom_normalize r p)
⊦ ∀M M' f f1 f2 f3.
M = M' ∧ (∀a. M' = canonical.SPvar a ⇒ f a = f' a) ∧
(∀a. M' = canonical.SPconst a ⇒ f1 a = f1' a) ∧
(∀a0 a1. M' = canonical.SPplus a0 a1 ⇒ f2 a0 a1 = f2' a0 a1) ∧
(∀a0 a1. M' = canonical.SPmult a0 a1 ⇒ f3 a0 a1 = f3' a0 a1) ⇒
canonical.spolynom_CASE M f f1 f2 f3 =
canonical.spolynom_CASE M' f' f1' f2' f3'
⊦ (∀f a.
ringNorm.polynom_size f (ringNorm.Pvar a) = 1 + quote.index_size a) ∧
(∀f a. ringNorm.polynom_size f (ringNorm.Pconst a) = 1 + f a) ∧
(∀f a0 a1.
ringNorm.polynom_size f (ringNorm.Pplus a0 a1) =
1 + (ringNorm.polynom_size f a0 + ringNorm.polynom_size f a1)) ∧
(∀f a0 a1.
ringNorm.polynom_size f (ringNorm.Pmult a0 a1) =
1 + (ringNorm.polynom_size f a0 + ringNorm.polynom_size f a1)) ∧
∀f a.
ringNorm.polynom_size f (ringNorm.Popp a) =
1 + ringNorm.polynom_size f a
⊦ (∀a a0 f f0 f1. ring.ring_R0 (ring.recordtype.ring a a0 f f0 f1) = a) ∧
(∀a a0 f f0 f1. ring.ring_R1 (ring.recordtype.ring a a0 f f0 f1) = a0) ∧
(∀a a0 f f0 f1. ring.ring_RP (ring.recordtype.ring a a0 f f0 f1) = f) ∧
(∀a a0 f f0 f1. ring.ring_RM (ring.recordtype.ring a a0 f f0 f1) = f0) ∧
∀a a0 f f0 f1. ring.ring_RN (ring.recordtype.ring a a0 f f0 f1) = f1
⊦ quote.index_compare quote.End_idx quote.End_idx = prelim.EQUAL ∧
(∀v10.
quote.index_compare quote.End_idx (quote.Left_idx v10) =
prelim.LESS) ∧
(∀v11.
quote.index_compare quote.End_idx (quote.Right_idx v11) =
prelim.LESS) ∧
(∀v2.
quote.index_compare (quote.Left_idx v2) quote.End_idx =
prelim.GREATER) ∧
(∀v3.
quote.index_compare (quote.Right_idx v3) quote.End_idx =
prelim.GREATER) ∧
(∀n' m'.
quote.index_compare (quote.Left_idx n') (quote.Left_idx m') =
quote.index_compare n' m') ∧
(∀n' m'.
quote.index_compare (quote.Left_idx n') (quote.Right_idx m') =
prelim.LESS) ∧
(∀n' m'.
quote.index_compare (quote.Right_idx n') (quote.Right_idx m') =
quote.index_compare n' m') ∧
∀n' m'.
quote.index_compare (quote.Right_idx n') (quote.Left_idx m') =
prelim.GREATER
⊦ (∀f1 a a0 f f0.
semi_ring.semi_ring_SR0_fupd f1
(semi_ring.recordtype.semi_ring a a0 f f0) =
semi_ring.recordtype.semi_ring (f1 a) a0 f f0) ∧
(∀f1 a a0 f f0.
semi_ring.semi_ring_SR1_fupd f1
(semi_ring.recordtype.semi_ring a a0 f f0) =
semi_ring.recordtype.semi_ring a (f1 a0) f f0) ∧
(∀f1 a a0 f f0.
semi_ring.semi_ring_SRP_fupd f1
(semi_ring.recordtype.semi_ring a a0 f f0) =
semi_ring.recordtype.semi_ring a a0 (f1 f) f0) ∧
∀f1 a a0 f f0.
semi_ring.semi_ring_SRM_fupd f1
(semi_ring.recordtype.semi_ring a a0 f f0) =
semi_ring.recordtype.semi_ring a a0 f (f1 f0)
⊦ ∀r.
(∀t2 l2 l1 c2.
ringNorm.r_varlist_insert r l1 (canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1 (canonical.Cons_monom c2 l2 t2))
(canonical.Cons_monom (ring.ring_RP r (ring.ring_R1 r) c2) l1 t2)
(canonical.Cons_monom c2 l2
(ringNorm.r_varlist_insert r l1 t2))) ∧
(∀t2 l2 l1.
ringNorm.r_varlist_insert r l1 (canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1 (canonical.Cons_varlist l2 t2))
(canonical.Cons_monom
(ring.ring_RP r (ring.ring_R1 r) (ring.ring_R1 r)) l1 t2)
(canonical.Cons_varlist l2 (ringNorm.r_varlist_insert r l1 t2))) ∧
∀l1.
ringNorm.r_varlist_insert r l1 canonical.Nil_monom =
canonical.Cons_varlist l1 canonical.Nil_monom
⊦ (∀r vm c. ringNorm.interp_p r vm (ringNorm.Pconst c) = c) ∧
(∀r vm i.
ringNorm.interp_p r vm (ringNorm.Pvar i) = quote.varmap_find i vm) ∧
(∀r vm p1 p2.
ringNorm.interp_p r vm (ringNorm.Pplus p1 p2) =
ring.ring_RP r (ringNorm.interp_p r vm p1)
(ringNorm.interp_p r vm p2)) ∧
(∀r vm p1 p2.
ringNorm.interp_p r vm (ringNorm.Pmult p1 p2) =
ring.ring_RM r (ringNorm.interp_p r vm p1)
(ringNorm.interp_p r vm p2)) ∧
∀r vm p1.
ringNorm.interp_p r vm (ringNorm.Popp p1) =
ring.ring_RN r (ringNorm.interp_p r vm p1)
⊦ (∀t2 sr l2 l1 c2.
canonical.varlist_insert sr l1 (canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1 (canonical.Cons_monom c2 l2 t2))
(canonical.Cons_monom
(semi_ring.semi_ring_SRP sr (semi_ring.semi_ring_SR1 sr) c2) l1
t2)
(canonical.Cons_monom c2 l2 (canonical.varlist_insert sr l1 t2))) ∧
(∀t2 sr l2 l1.
canonical.varlist_insert sr l1 (canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1 (canonical.Cons_varlist l2 t2))
(canonical.Cons_monom
(semi_ring.semi_ring_SRP sr (semi_ring.semi_ring_SR1 sr)
(semi_ring.semi_ring_SR1 sr)) l1 t2)
(canonical.Cons_varlist l2 (canonical.varlist_insert sr l1 t2))) ∧
∀sr l1.
canonical.varlist_insert sr l1 canonical.Nil_monom =
canonical.Cons_varlist l1 canonical.Nil_monom
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0'.
∀'spolynom'.
(∀a0'.
(∃a.
a0' =
let a ← a in
ind_type.CONSTR 0 (a, bool.ARB) (λn. ind_type.BOTTOM)) ∨
(∃a.
a0' =
let a ← a in
ind_type.CONSTR (suc 0) (bool.ARB, a)
(λn. ind_type.BOTTOM)) ∨
(∃a0 a1.
a0' =
(let a0 ← a0 in
λa1.
ind_type.CONSTR (suc (suc 0)) (bool.ARB, bool.ARB)
(ind_type.FCONS a0
(ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1 ∧
'spolynom' a0 ∧ 'spolynom' a1) ∨
(∃a0 a1.
a0' =
(let a0 ← a0 in
λa1.
ind_type.CONSTR (suc (suc (suc 0)))
(bool.ARB, bool.ARB)
(ind_type.FCONS a0
(ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1 ∧
'spolynom' a0 ∧ 'spolynom' a1) ⇒ 'spolynom' a0') ⇒
'spolynom' a0') rep
⊦ (∀x. x = x ⇔ ⊤) ∧
(prelim.ordering2num prelim.LESS = 0 ∧
prelim.ordering2num prelim.EQUAL = 1 ∧
prelim.ordering2num prelim.GREATER = arithmetic.BIT2 0) ∧
((∀v0 v1 v2. prelim.ordering_CASE prelim.LESS v0 v1 v2 = v0) ∧
(∀v0 v1 v2. prelim.ordering_CASE prelim.EQUAL v0 v1 v2 = v1) ∧
∀v0 v1 v2. prelim.ordering_CASE prelim.GREATER v0 v1 v2 = v2) ∧
(prelim.LESS = prelim.EQUAL ⇔ ⊥) ∧ (prelim.LESS = prelim.GREATER ⇔ ⊥) ∧
(prelim.EQUAL = prelim.GREATER ⇔ ⊥) ∧ (prelim.EQUAL = prelim.LESS ⇔ ⊥) ∧
(prelim.GREATER = prelim.LESS ⇔ ⊥) ∧ (prelim.GREATER = prelim.EQUAL ⇔ ⊥)
⊦ (∀s g f.
semi_ring.semi_ring_SR1_fupd f (semi_ring.semi_ring_SR0_fupd g s) =
semi_ring.semi_ring_SR0_fupd g (semi_ring.semi_ring_SR1_fupd f s)) ∧
(∀s g f.
semi_ring.semi_ring_SRP_fupd f (semi_ring.semi_ring_SR0_fupd g s) =
semi_ring.semi_ring_SR0_fupd g (semi_ring.semi_ring_SRP_fupd f s)) ∧
(∀s g f.
semi_ring.semi_ring_SRP_fupd f (semi_ring.semi_ring_SR1_fupd g s) =
semi_ring.semi_ring_SR1_fupd g (semi_ring.semi_ring_SRP_fupd f s)) ∧
(∀s g f.
semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SR0_fupd g s) =
semi_ring.semi_ring_SR0_fupd g (semi_ring.semi_ring_SRM_fupd f s)) ∧
(∀s g f.
semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SR1_fupd g s) =
semi_ring.semi_ring_SR1_fupd g (semi_ring.semi_ring_SRM_fupd f s)) ∧
∀s g f.
semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SRP_fupd g s) =
semi_ring.semi_ring_SRP_fupd g (semi_ring.semi_ring_SRM_fupd f s)
⊦ ∀r.
(∀t2 l2 l1 c2 c1.
ringNorm.r_monom_insert r c1 l1 (canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1 (canonical.Cons_monom c2 l2 t2))
(canonical.Cons_monom (ring.ring_RP r c1 c2) l1 t2)
(canonical.Cons_monom c2 l2
(ringNorm.r_monom_insert r c1 l1 t2))) ∧
(∀t2 l2 l1 c1.
ringNorm.r_monom_insert r c1 l1 (canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1 (canonical.Cons_varlist l2 t2))
(canonical.Cons_monom (ring.ring_RP r c1 (ring.ring_R1 r)) l1 t2)
(canonical.Cons_varlist l2
(ringNorm.r_monom_insert r c1 l1 t2))) ∧
∀l1 c1.
ringNorm.r_monom_insert r c1 l1 canonical.Nil_monom =
canonical.Cons_monom c1 l1 canonical.Nil_monom
⊦ ∀M M' f f1 f2 f3 f4.
M = M' ∧ (∀a. M' = ringNorm.Pvar a ⇒ f a = f' a) ∧
(∀a. M' = ringNorm.Pconst a ⇒ f1 a = f1' a) ∧
(∀a0 a1. M' = ringNorm.Pplus a0 a1 ⇒ f2 a0 a1 = f2' a0 a1) ∧
(∀a0 a1. M' = ringNorm.Pmult a0 a1 ⇒ f3 a0 a1 = f3' a0 a1) ∧
(∀a. M' = ringNorm.Popp a ⇒ f4 a = f4' a) ⇒
ringNorm.polynom_CASE M f f1 f2 f3 f4 =
ringNorm.polynom_CASE M' f' f1' f2' f3' f4'
⊦ (∀t2 sr l2 l1 c2 c1.
canonical.monom_insert sr c1 l1 (canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1 (canonical.Cons_monom c2 l2 t2))
(canonical.Cons_monom (semi_ring.semi_ring_SRP sr c1 c2) l1 t2)
(canonical.Cons_monom c2 l2 (canonical.monom_insert sr c1 l1 t2))) ∧
(∀t2 sr l2 l1 c1.
canonical.monom_insert sr c1 l1 (canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1 (canonical.Cons_varlist l2 t2))
(canonical.Cons_monom
(semi_ring.semi_ring_SRP sr c1 (semi_ring.semi_ring_SR1 sr)) l1
t2)
(canonical.Cons_varlist l2 (canonical.monom_insert sr c1 l1 t2))) ∧
∀sr l1 c1.
canonical.monom_insert sr c1 l1 canonical.Nil_monom =
canonical.Cons_monom c1 l1 canonical.Nil_monom
⊦ prelim.list_merge_tupled =
relation.WFREC
(select R.
wellFounded R ∧
(∀l2 l1 y x a_lt.
¬a_lt x y ⇒ R (a_lt, x :: l1, l2) (a_lt, x :: l1, y :: l2)) ∧
∀l2 l1 y x a_lt.
a_lt x y ⇒ R (a_lt, l1, y :: l2) (a_lt, x :: l1, y :: l2))
(λlist_merge_tupled a.
pair.pair_CASE a
(λa_lt v1.
pair.pair_CASE v1
(λl1 v3.
list.list_CASE v3 (id l1)
(λy l2.
list.list_CASE l1 (id (y :: l2))
(λx l1'.
id
(if a_lt x y then
x :: list_merge_tupled (a_lt, l1', y :: l2)
else
y ::
list_merge_tupled
(a_lt, x :: l1', l2)))))))
⊦ (∀a f f1 f2 f3 f4.
ringNorm.polynom_CASE (ringNorm.Pvar a) f f1 f2 f3 f4 = f a) ∧
(∀a f f1 f2 f3 f4.
ringNorm.polynom_CASE (ringNorm.Pconst a) f f1 f2 f3 f4 = f1 a) ∧
(∀a0 a1 f f1 f2 f3 f4.
ringNorm.polynom_CASE (ringNorm.Pplus a0 a1) f f1 f2 f3 f4 =
f2 a0 a1) ∧
(∀a0 a1 f f1 f2 f3 f4.
ringNorm.polynom_CASE (ringNorm.Pmult a0 a1) f f1 f2 f3 f4 =
f3 a0 a1) ∧
∀a f f1 f2 f3 f4.
ringNorm.polynom_CASE (ringNorm.Popp a) f f1 f2 f3 f4 = f4 a
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0'.
∀'polynom'.
(∀a0'.
(∃a.
a0' =
let a ← a in
ind_type.CONSTR 0 (a, bool.ARB) (λn. ind_type.BOTTOM)) ∨
(∃a.
a0' =
let a ← a in
ind_type.CONSTR (suc 0) (bool.ARB, a)
(λn. ind_type.BOTTOM)) ∨
(∃a0 a1.
a0' =
(let a0 ← a0 in
λa1.
ind_type.CONSTR (suc (suc 0)) (bool.ARB, bool.ARB)
(ind_type.FCONS a0
(ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1 ∧
'polynom' a0 ∧ 'polynom' a1) ∨
(∃a0 a1.
a0' =
(let a0 ← a0 in
λa1.
ind_type.CONSTR (suc (suc (suc 0)))
(bool.ARB, bool.ARB)
(ind_type.FCONS a0
(ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1 ∧
'polynom' a0 ∧ 'polynom' a1) ∨
(∃a.
a0' =
(let a ← a in
ind_type.CONSTR (suc (suc (suc (suc 0))))
(bool.ARB, bool.ARB)
(ind_type.FCONS a (λn. ind_type.BOTTOM))) ∧
'polynom' a) ⇒ 'polynom' a0') ⇒ 'polynom' a0') rep
⊦ (∀a' a. ¬(ringNorm.Pvar a = ringNorm.Pconst a')) ∧
(∀a1 a0 a. ¬(ringNorm.Pvar a = ringNorm.Pplus a0 a1)) ∧
(∀a1 a0 a. ¬(ringNorm.Pvar a = ringNorm.Pmult a0 a1)) ∧
(∀a' a. ¬(ringNorm.Pvar a = ringNorm.Popp a')) ∧
(∀a1 a0 a. ¬(ringNorm.Pconst a = ringNorm.Pplus a0 a1)) ∧
(∀a1 a0 a. ¬(ringNorm.Pconst a = ringNorm.Pmult a0 a1)) ∧
(∀a' a. ¬(ringNorm.Pconst a = ringNorm.Popp a')) ∧
(∀a1' a1 a0' a0. ¬(ringNorm.Pplus a0 a1 = ringNorm.Pmult a0' a1')) ∧
(∀a1 a0 a. ¬(ringNorm.Pplus a0 a1 = ringNorm.Popp a)) ∧
∀a1 a0 a. ¬(ringNorm.Pmult a0 a1 = ringNorm.Popp a)
⊦ ∀r.
semi_ring.is_semi_ring r ⇔
(∀n m. semi_ring.semi_ring_SRP r n m = semi_ring.semi_ring_SRP r m n) ∧
(∀n m p.
semi_ring.semi_ring_SRP r n (semi_ring.semi_ring_SRP r m p) =
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r n m) p) ∧
(∀n m. semi_ring.semi_ring_SRM r n m = semi_ring.semi_ring_SRM r m n) ∧
(∀n m p.
semi_ring.semi_ring_SRM r n (semi_ring.semi_ring_SRM r m p) =
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r n m) p) ∧
(∀n. semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SR0 r) n = n) ∧
(∀n. semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SR1 r) n = n) ∧
(∀n.
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SR0 r) n =
semi_ring.semi_ring_SR0 r) ∧
∀n m p.
semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRP r n m) p =
semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRM r n p)
(semi_ring.semi_ring_SRM r m p)
⊦ ∀r.
ring.is_ring r ⇔
(∀n m. ring.ring_RP r n m = ring.ring_RP r m n) ∧
(∀n m p.
ring.ring_RP r n (ring.ring_RP r m p) =
ring.ring_RP r (ring.ring_RP r n m) p) ∧
(∀n m. ring.ring_RM r n m = ring.ring_RM r m n) ∧
(∀n m p.
ring.ring_RM r n (ring.ring_RM r m p) =
ring.ring_RM r (ring.ring_RM r n m) p) ∧
(∀n. ring.ring_RP r (ring.ring_R0 r) n = n) ∧
(∀n. ring.ring_RM r (ring.ring_R1 r) n = n) ∧
(∀n. ring.ring_RP r n (ring.ring_RN r n) = ring.ring_R0 r) ∧
∀n m p.
ring.ring_RM r (ring.ring_RP r n m) p =
ring.ring_RP r (ring.ring_RM r n p) (ring.ring_RM r m p)
⊦ (∀f2 a a0 f f0 f1.
ring.ring_R0_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring (f2 a) a0 f f0 f1) ∧
(∀f2 a a0 f f0 f1.
ring.ring_R1_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring a (f2 a0) f f0 f1) ∧
(∀f2 a a0 f f0 f1.
ring.ring_RP_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring a a0 (f2 f) f0 f1) ∧
(∀f2 a a0 f f0 f1.
ring.ring_RM_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring a a0 f (f2 f0) f1) ∧
∀f2 a a0 f f0 f1.
ring.ring_RN_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
ring.recordtype.ring a a0 f f0 (f2 f1)
⊦ ((∀g f.
semi_ring.semi_ring_SR0_fupd f ∘ semi_ring.semi_ring_SR0_fupd g =
semi_ring.semi_ring_SR0_fupd (f ∘ g)) ∧
∀h g f.
semi_ring.semi_ring_SR0_fupd f ∘
(semi_ring.semi_ring_SR0_fupd g ∘ h) =
semi_ring.semi_ring_SR0_fupd (f ∘ g) ∘ h) ∧
((∀g f.
semi_ring.semi_ring_SR1_fupd f ∘ semi_ring.semi_ring_SR1_fupd g =
semi_ring.semi_ring_SR1_fupd (f ∘ g)) ∧
∀h g f.
semi_ring.semi_ring_SR1_fupd f ∘
(semi_ring.semi_ring_SR1_fupd g ∘ h) =
semi_ring.semi_ring_SR1_fupd (f ∘ g) ∘ h) ∧
((∀g f.
semi_ring.semi_ring_SRP_fupd f ∘ semi_ring.semi_ring_SRP_fupd g =
semi_ring.semi_ring_SRP_fupd (f ∘ g)) ∧
∀h g f.
semi_ring.semi_ring_SRP_fupd f ∘
(semi_ring.semi_ring_SRP_fupd g ∘ h) =
semi_ring.semi_ring_SRP_fupd (f ∘ g) ∘ h) ∧
(∀g f.
semi_ring.semi_ring_SRM_fupd f ∘ semi_ring.semi_ring_SRM_fupd g =
semi_ring.semi_ring_SRM_fupd (f ∘ g)) ∧
∀h g f.
semi_ring.semi_ring_SRM_fupd f ∘ (semi_ring.semi_ring_SRM_fupd g ∘ h) =
semi_ring.semi_ring_SRM_fupd (f ∘ g) ∘ h
⊦ (∀r g f.
ring.ring_R1_fupd f (ring.ring_R0_fupd g r) =
ring.ring_R0_fupd g (ring.ring_R1_fupd f r)) ∧
(∀r g f.
ring.ring_RP_fupd f (ring.ring_R0_fupd g r) =
ring.ring_R0_fupd g (ring.ring_RP_fupd f r)) ∧
(∀r g f.
ring.ring_RP_fupd f (ring.ring_R1_fupd g r) =
ring.ring_R1_fupd g (ring.ring_RP_fupd f r)) ∧
(∀r g f.
ring.ring_RM_fupd f (ring.ring_R0_fupd g r) =
ring.ring_R0_fupd g (ring.ring_RM_fupd f r)) ∧
(∀r g f.
ring.ring_RM_fupd f (ring.ring_R1_fupd g r) =
ring.ring_R1_fupd g (ring.ring_RM_fupd f r)) ∧
(∀r g f.
ring.ring_RM_fupd f (ring.ring_RP_fupd g r) =
ring.ring_RP_fupd g (ring.ring_RM_fupd f r)) ∧
(∀r g f.
ring.ring_RN_fupd f (ring.ring_R0_fupd g r) =
ring.ring_R0_fupd g (ring.ring_RN_fupd f r)) ∧
(∀r g f.
ring.ring_RN_fupd f (ring.ring_R1_fupd g r) =
ring.ring_R1_fupd g (ring.ring_RN_fupd f r)) ∧
(∀r g f.
ring.ring_RN_fupd f (ring.ring_RP_fupd g r) =
ring.ring_RP_fupd g (ring.ring_RN_fupd f r)) ∧
∀r g f.
ring.ring_RN_fupd f (ring.ring_RM_fupd g r) =
ring.ring_RM_fupd g (ring.ring_RN_fupd f r)
⊦ ((∀g f.
ring.ring_R0_fupd f ∘ ring.ring_R0_fupd g =
ring.ring_R0_fupd (f ∘ g)) ∧
∀h g f.
ring.ring_R0_fupd f ∘ (ring.ring_R0_fupd g ∘ h) =
ring.ring_R0_fupd (f ∘ g) ∘ h) ∧
((∀g f.
ring.ring_R1_fupd f ∘ ring.ring_R1_fupd g =
ring.ring_R1_fupd (f ∘ g)) ∧
∀h g f.
ring.ring_R1_fupd f ∘ (ring.ring_R1_fupd g ∘ h) =
ring.ring_R1_fupd (f ∘ g) ∘ h) ∧
((∀g f.
ring.ring_RP_fupd f ∘ ring.ring_RP_fupd g =
ring.ring_RP_fupd (f ∘ g)) ∧
∀h g f.
ring.ring_RP_fupd f ∘ (ring.ring_RP_fupd g ∘ h) =
ring.ring_RP_fupd (f ∘ g) ∘ h) ∧
((∀g f.
ring.ring_RM_fupd f ∘ ring.ring_RM_fupd g =
ring.ring_RM_fupd (f ∘ g)) ∧
∀h g f.
ring.ring_RM_fupd f ∘ (ring.ring_RM_fupd g ∘ h) =
ring.ring_RM_fupd (f ∘ g) ∘ h) ∧
(∀g f.
ring.ring_RN_fupd f ∘ ring.ring_RN_fupd g =
ring.ring_RN_fupd (f ∘ g)) ∧
∀h g f.
ring.ring_RN_fupd f ∘ (ring.ring_RN_fupd g ∘ h) =
ring.ring_RN_fupd (f ∘ g) ∘ h
⊦ (∀s f.
semi_ring.semi_ring_SR0 (semi_ring.semi_ring_SR1_fupd f s) =
semi_ring.semi_ring_SR0 s) ∧
(∀s f.
semi_ring.semi_ring_SR0 (semi_ring.semi_ring_SRP_fupd f s) =
semi_ring.semi_ring_SR0 s) ∧
(∀s f.
semi_ring.semi_ring_SR0 (semi_ring.semi_ring_SRM_fupd f s) =
semi_ring.semi_ring_SR0 s) ∧
(∀s f.
semi_ring.semi_ring_SR1 (semi_ring.semi_ring_SR0_fupd f s) =
semi_ring.semi_ring_SR1 s) ∧
(∀s f.
semi_ring.semi_ring_SR1 (semi_ring.semi_ring_SRP_fupd f s) =
semi_ring.semi_ring_SR1 s) ∧
(∀s f.
semi_ring.semi_ring_SR1 (semi_ring.semi_ring_SRM_fupd f s) =
semi_ring.semi_ring_SR1 s) ∧
(∀s f.
semi_ring.semi_ring_SRP (semi_ring.semi_ring_SR0_fupd f s) =
semi_ring.semi_ring_SRP s) ∧
(∀s f.
semi_ring.semi_ring_SRP (semi_ring.semi_ring_SR1_fupd f s) =
semi_ring.semi_ring_SRP s) ∧
(∀s f.
semi_ring.semi_ring_SRP (semi_ring.semi_ring_SRM_fupd f s) =
semi_ring.semi_ring_SRP s) ∧
(∀s f.
semi_ring.semi_ring_SRM (semi_ring.semi_ring_SR0_fupd f s) =
semi_ring.semi_ring_SRM s) ∧
(∀s f.
semi_ring.semi_ring_SRM (semi_ring.semi_ring_SR1_fupd f s) =
semi_ring.semi_ring_SRM s) ∧
(∀s f.
semi_ring.semi_ring_SRM (semi_ring.semi_ring_SRP_fupd f s) =
semi_ring.semi_ring_SRM s) ∧
(∀s f.
semi_ring.semi_ring_SR0 (semi_ring.semi_ring_SR0_fupd f s) =
f (semi_ring.semi_ring_SR0 s)) ∧
(∀s f.
semi_ring.semi_ring_SR1 (semi_ring.semi_ring_SR1_fupd f s) =
f (semi_ring.semi_ring_SR1 s)) ∧
(∀s f.
semi_ring.semi_ring_SRP (semi_ring.semi_ring_SRP_fupd f s) =
f (semi_ring.semi_ring_SRP s)) ∧
∀s f.
semi_ring.semi_ring_SRM (semi_ring.semi_ring_SRM_fupd f s) =
f (semi_ring.semi_ring_SRM s)
⊦ ∀P.
(∀sr c1 l1 t1 c2 l2 t2.
P sr t1 t2 ∧ P sr t1 (canonical.Cons_monom c2 l2 t2) ∧
P sr (canonical.Cons_monom c1 l1 t1) t2 ⇒
P sr (canonical.Cons_monom c1 l1 t1)
(canonical.Cons_monom c2 l2 t2)) ∧
(∀sr c1 l1 t1 l2 t2.
P sr t1 t2 ∧ P sr t1 (canonical.Cons_varlist l2 t2) ∧
P sr (canonical.Cons_monom c1 l1 t1) t2 ⇒
P sr (canonical.Cons_monom c1 l1 t1)
(canonical.Cons_varlist l2 t2)) ∧
(∀sr l1 t1 c2 l2 t2.
P sr t1 t2 ∧ P sr t1 (canonical.Cons_monom c2 l2 t2) ∧
P sr (canonical.Cons_varlist l1 t1) t2 ⇒
P sr (canonical.Cons_varlist l1 t1)
(canonical.Cons_monom c2 l2 t2)) ∧
(∀sr l1 t1 l2 t2.
P sr t1 t2 ∧ P sr t1 (canonical.Cons_varlist l2 t2) ∧
P sr (canonical.Cons_varlist l1 t1) t2 ⇒
P sr (canonical.Cons_varlist l1 t1)
(canonical.Cons_varlist l2 t2)) ∧
(∀sr s1. P sr s1 canonical.Nil_monom) ∧
(∀sr v4 v5 v6.
P sr canonical.Nil_monom (canonical.Cons_monom v4 v5 v6)) ∧
(∀sr v7 v8. P sr canonical.Nil_monom (canonical.Cons_varlist v7 v8)) ⇒
∀v v1 v2. P v v1 v2
⊦ ((∀g f.
semi_ring.semi_ring_SR1_fupd f ∘ semi_ring.semi_ring_SR0_fupd g =
semi_ring.semi_ring_SR0_fupd g ∘ semi_ring.semi_ring_SR1_fupd f) ∧
∀h g f.
semi_ring.semi_ring_SR1_fupd f ∘
(semi_ring.semi_ring_SR0_fupd g ∘ h) =
semi_ring.semi_ring_SR0_fupd g ∘
(semi_ring.semi_ring_SR1_fupd f ∘ h)) ∧
((∀g f.
semi_ring.semi_ring_SRP_fupd f ∘ semi_ring.semi_ring_SR0_fupd g =
semi_ring.semi_ring_SR0_fupd g ∘ semi_ring.semi_ring_SRP_fupd f) ∧
∀h g f.
semi_ring.semi_ring_SRP_fupd f ∘
(semi_ring.semi_ring_SR0_fupd g ∘ h) =
semi_ring.semi_ring_SR0_fupd g ∘
(semi_ring.semi_ring_SRP_fupd f ∘ h)) ∧
((∀g f.
semi_ring.semi_ring_SRP_fupd f ∘ semi_ring.semi_ring_SR1_fupd g =
semi_ring.semi_ring_SR1_fupd g ∘ semi_ring.semi_ring_SRP_fupd f) ∧
∀h g f.
semi_ring.semi_ring_SRP_fupd f ∘
(semi_ring.semi_ring_SR1_fupd g ∘ h) =
semi_ring.semi_ring_SR1_fupd g ∘
(semi_ring.semi_ring_SRP_fupd f ∘ h)) ∧
((∀g f.
semi_ring.semi_ring_SRM_fupd f ∘ semi_ring.semi_ring_SR0_fupd g =
semi_ring.semi_ring_SR0_fupd g ∘ semi_ring.semi_ring_SRM_fupd f) ∧
∀h g f.
semi_ring.semi_ring_SRM_fupd f ∘
(semi_ring.semi_ring_SR0_fupd g ∘ h) =
semi_ring.semi_ring_SR0_fupd g ∘
(semi_ring.semi_ring_SRM_fupd f ∘ h)) ∧
((∀g f.
semi_ring.semi_ring_SRM_fupd f ∘ semi_ring.semi_ring_SR1_fupd g =
semi_ring.semi_ring_SR1_fupd g ∘ semi_ring.semi_ring_SRM_fupd f) ∧
∀h g f.
semi_ring.semi_ring_SRM_fupd f ∘
(semi_ring.semi_ring_SR1_fupd g ∘ h) =
semi_ring.semi_ring_SR1_fupd g ∘
(semi_ring.semi_ring_SRM_fupd f ∘ h)) ∧
(∀g f.
semi_ring.semi_ring_SRM_fupd f ∘ semi_ring.semi_ring_SRP_fupd g =
semi_ring.semi_ring_SRP_fupd g ∘ semi_ring.semi_ring_SRM_fupd f) ∧
∀h g f.
semi_ring.semi_ring_SRM_fupd f ∘ (semi_ring.semi_ring_SRP_fupd g ∘ h) =
semi_ring.semi_ring_SRP_fupd g ∘ (semi_ring.semi_ring_SRM_fupd f ∘ h)
⊦ ∀r.
(∀t2 t1 l2 l1 c2 c1.
ringNorm.r_canonical_sum_merge r (canonical.Cons_monom c1 l1 t1)
(canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1
(ringNorm.r_canonical_sum_merge r t1
(canonical.Cons_monom c2 l2 t2)))
(canonical.Cons_monom (ring.ring_RP r c1 c2) l1
(ringNorm.r_canonical_sum_merge r t1 t2))
(canonical.Cons_monom c2 l2
(ringNorm.r_canonical_sum_merge r
(canonical.Cons_monom c1 l1 t1) t2))) ∧
(∀t2 t1 l2 l1 c1.
ringNorm.r_canonical_sum_merge r (canonical.Cons_monom c1 l1 t1)
(canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1
(ringNorm.r_canonical_sum_merge r t1
(canonical.Cons_varlist l2 t2)))
(canonical.Cons_monom (ring.ring_RP r c1 (ring.ring_R1 r)) l1
(ringNorm.r_canonical_sum_merge r t1 t2))
(canonical.Cons_varlist l2
(ringNorm.r_canonical_sum_merge r
(canonical.Cons_monom c1 l1 t1) t2))) ∧
(∀t2 t1 l2 l1 c2.
ringNorm.r_canonical_sum_merge r (canonical.Cons_varlist l1 t1)
(canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1
(ringNorm.r_canonical_sum_merge r t1
(canonical.Cons_monom c2 l2 t2)))
(canonical.Cons_monom (ring.ring_RP r (ring.ring_R1 r) c2) l1
(ringNorm.r_canonical_sum_merge r t1 t2))
(canonical.Cons_monom c2 l2
(ringNorm.r_canonical_sum_merge r
(canonical.Cons_varlist l1 t1) t2))) ∧
(∀t2 t1 l2 l1.
ringNorm.r_canonical_sum_merge r (canonical.Cons_varlist l1 t1)
(canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1
(ringNorm.r_canonical_sum_merge r t1
(canonical.Cons_varlist l2 t2)))
(canonical.Cons_monom
(ring.ring_RP r (ring.ring_R1 r) (ring.ring_R1 r)) l1
(ringNorm.r_canonical_sum_merge r t1 t2))
(canonical.Cons_varlist l2
(ringNorm.r_canonical_sum_merge r
(canonical.Cons_varlist l1 t1) t2))) ∧
(∀s1. ringNorm.r_canonical_sum_merge r s1 canonical.Nil_monom = s1) ∧
(∀v6 v5 v4.
ringNorm.r_canonical_sum_merge r canonical.Nil_monom
(canonical.Cons_monom v4 v5 v6) = canonical.Cons_monom v4 v5 v6) ∧
∀v8 v7.
ringNorm.r_canonical_sum_merge r canonical.Nil_monom
(canonical.Cons_varlist v7 v8) = canonical.Cons_varlist v7 v8
⊦ (∀t2 t1 sr l2 l1 c2 c1.
canonical.canonical_sum_merge sr (canonical.Cons_monom c1 l1 t1)
(canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1
(canonical.canonical_sum_merge sr t1
(canonical.Cons_monom c2 l2 t2)))
(canonical.Cons_monom (semi_ring.semi_ring_SRP sr c1 c2) l1
(canonical.canonical_sum_merge sr t1 t2))
(canonical.Cons_monom c2 l2
(canonical.canonical_sum_merge sr (canonical.Cons_monom c1 l1 t1)
t2))) ∧
(∀t2 t1 sr l2 l1 c1.
canonical.canonical_sum_merge sr (canonical.Cons_monom c1 l1 t1)
(canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1
(canonical.canonical_sum_merge sr t1
(canonical.Cons_varlist l2 t2)))
(canonical.Cons_monom
(semi_ring.semi_ring_SRP sr c1 (semi_ring.semi_ring_SR1 sr)) l1
(canonical.canonical_sum_merge sr t1 t2))
(canonical.Cons_varlist l2
(canonical.canonical_sum_merge sr (canonical.Cons_monom c1 l1 t1)
t2))) ∧
(∀t2 t1 sr l2 l1 c2.
canonical.canonical_sum_merge sr (canonical.Cons_varlist l1 t1)
(canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1
(canonical.canonical_sum_merge sr t1
(canonical.Cons_monom c2 l2 t2)))
(canonical.Cons_monom
(semi_ring.semi_ring_SRP sr (semi_ring.semi_ring_SR1 sr) c2) l1
(canonical.canonical_sum_merge sr t1 t2))
(canonical.Cons_monom c2 l2
(canonical.canonical_sum_merge sr (canonical.Cons_varlist l1 t1)
t2))) ∧
(∀t2 t1 sr l2 l1.
canonical.canonical_sum_merge sr (canonical.Cons_varlist l1 t1)
(canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1
(canonical.canonical_sum_merge sr t1
(canonical.Cons_varlist l2 t2)))
(canonical.Cons_monom
(semi_ring.semi_ring_SRP sr (semi_ring.semi_ring_SR1 sr)
(semi_ring.semi_ring_SR1 sr)) l1
(canonical.canonical_sum_merge sr t1 t2))
(canonical.Cons_varlist l2
(canonical.canonical_sum_merge sr (canonical.Cons_varlist l1 t1)
t2))) ∧
(∀sr s1. canonical.canonical_sum_merge sr s1 canonical.Nil_monom = s1) ∧
(∀v6 v5 v4 sr.
canonical.canonical_sum_merge sr canonical.Nil_monom
(canonical.Cons_monom v4 v5 v6) = canonical.Cons_monom v4 v5 v6) ∧
∀v8 v7 sr.
canonical.canonical_sum_merge sr canonical.Nil_monom
(canonical.Cons_varlist v7 v8) = canonical.Cons_varlist v7 v8
⊦ (∀r f. ring.ring_R0 (ring.ring_R1_fupd f r) = ring.ring_R0 r) ∧
(∀r f. ring.ring_R0 (ring.ring_RP_fupd f r) = ring.ring_R0 r) ∧
(∀r f. ring.ring_R0 (ring.ring_RM_fupd f r) = ring.ring_R0 r) ∧
(∀r f. ring.ring_R0 (ring.ring_RN_fupd f r) = ring.ring_R0 r) ∧
(∀r f. ring.ring_R1 (ring.ring_R0_fupd f r) = ring.ring_R1 r) ∧
(∀r f. ring.ring_R1 (ring.ring_RP_fupd f r) = ring.ring_R1 r) ∧
(∀r f. ring.ring_R1 (ring.ring_RM_fupd f r) = ring.ring_R1 r) ∧
(∀r f. ring.ring_R1 (ring.ring_RN_fupd f r) = ring.ring_R1 r) ∧
(∀r f. ring.ring_RP (ring.ring_R0_fupd f r) = ring.ring_RP r) ∧
(∀r f. ring.ring_RP (ring.ring_R1_fupd f r) = ring.ring_RP r) ∧
(∀r f. ring.ring_RP (ring.ring_RM_fupd f r) = ring.ring_RP r) ∧
(∀r f. ring.ring_RP (ring.ring_RN_fupd f r) = ring.ring_RP r) ∧
(∀r f. ring.ring_RM (ring.ring_R0_fupd f r) = ring.ring_RM r) ∧
(∀r f. ring.ring_RM (ring.ring_R1_fupd f r) = ring.ring_RM r) ∧
(∀r f. ring.ring_RM (ring.ring_RP_fupd f r) = ring.ring_RM r) ∧
(∀r f. ring.ring_RM (ring.ring_RN_fupd f r) = ring.ring_RM r) ∧
(∀r f. ring.ring_RN (ring.ring_R0_fupd f r) = ring.ring_RN r) ∧
(∀r f. ring.ring_RN (ring.ring_R1_fupd f r) = ring.ring_RN r) ∧
(∀r f. ring.ring_RN (ring.ring_RP_fupd f r) = ring.ring_RN r) ∧
(∀r f. ring.ring_RN (ring.ring_RM_fupd f r) = ring.ring_RN r) ∧
(∀r f. ring.ring_R0 (ring.ring_R0_fupd f r) = f (ring.ring_R0 r)) ∧
(∀r f. ring.ring_R1 (ring.ring_R1_fupd f r) = f (ring.ring_R1 r)) ∧
(∀r f. ring.ring_RP (ring.ring_RP_fupd f r) = f (ring.ring_RP r)) ∧
(∀r f. ring.ring_RM (ring.ring_RM_fupd f r) = f (ring.ring_RM r)) ∧
∀r f. ring.ring_RN (ring.ring_RN_fupd f r) = f (ring.ring_RN r)
⊦ ((∀g f.
ring.ring_R1_fupd f ∘ ring.ring_R0_fupd g =
ring.ring_R0_fupd g ∘ ring.ring_R1_fupd f) ∧
∀h g f.
ring.ring_R1_fupd f ∘ (ring.ring_R0_fupd g ∘ h) =
ring.ring_R0_fupd g ∘ (ring.ring_R1_fupd f ∘ h)) ∧
((∀g f.
ring.ring_RP_fupd f ∘ ring.ring_R0_fupd g =
ring.ring_R0_fupd g ∘ ring.ring_RP_fupd f) ∧
∀h g f.
ring.ring_RP_fupd f ∘ (ring.ring_R0_fupd g ∘ h) =
ring.ring_R0_fupd g ∘ (ring.ring_RP_fupd f ∘ h)) ∧
((∀g f.
ring.ring_RP_fupd f ∘ ring.ring_R1_fupd g =
ring.ring_R1_fupd g ∘ ring.ring_RP_fupd f) ∧
∀h g f.
ring.ring_RP_fupd f ∘ (ring.ring_R1_fupd g ∘ h) =
ring.ring_R1_fupd g ∘ (ring.ring_RP_fupd f ∘ h)) ∧
((∀g f.
ring.ring_RM_fupd f ∘ ring.ring_R0_fupd g =
ring.ring_R0_fupd g ∘ ring.ring_RM_fupd f) ∧
∀h g f.
ring.ring_RM_fupd f ∘ (ring.ring_R0_fupd g ∘ h) =
ring.ring_R0_fupd g ∘ (ring.ring_RM_fupd f ∘ h)) ∧
((∀g f.
ring.ring_RM_fupd f ∘ ring.ring_R1_fupd g =
ring.ring_R1_fupd g ∘ ring.ring_RM_fupd f) ∧
∀h g f.
ring.ring_RM_fupd f ∘ (ring.ring_R1_fupd g ∘ h) =
ring.ring_R1_fupd g ∘ (ring.ring_RM_fupd f ∘ h)) ∧
((∀g f.
ring.ring_RM_fupd f ∘ ring.ring_RP_fupd g =
ring.ring_RP_fupd g ∘ ring.ring_RM_fupd f) ∧
∀h g f.
ring.ring_RM_fupd f ∘ (ring.ring_RP_fupd g ∘ h) =
ring.ring_RP_fupd g ∘ (ring.ring_RM_fupd f ∘ h)) ∧
((∀g f.
ring.ring_RN_fupd f ∘ ring.ring_R0_fupd g =
ring.ring_R0_fupd g ∘ ring.ring_RN_fupd f) ∧
∀h g f.
ring.ring_RN_fupd f ∘ (ring.ring_R0_fupd g ∘ h) =
ring.ring_R0_fupd g ∘ (ring.ring_RN_fupd f ∘ h)) ∧
((∀g f.
ring.ring_RN_fupd f ∘ ring.ring_R1_fupd g =
ring.ring_R1_fupd g ∘ ring.ring_RN_fupd f) ∧
∀h g f.
ring.ring_RN_fupd f ∘ (ring.ring_R1_fupd g ∘ h) =
ring.ring_R1_fupd g ∘ (ring.ring_RN_fupd f ∘ h)) ∧
((∀g f.
ring.ring_RN_fupd f ∘ ring.ring_RP_fupd g =
ring.ring_RP_fupd g ∘ ring.ring_RN_fupd f) ∧
∀h g f.
ring.ring_RN_fupd f ∘ (ring.ring_RP_fupd g ∘ h) =
ring.ring_RP_fupd g ∘ (ring.ring_RN_fupd f ∘ h)) ∧
(∀g f.
ring.ring_RN_fupd f ∘ ring.ring_RM_fupd g =
ring.ring_RM_fupd g ∘ ring.ring_RN_fupd f) ∧
∀h g f.
ring.ring_RN_fupd f ∘ (ring.ring_RM_fupd g ∘ h) =
ring.ring_RM_fupd g ∘ (ring.ring_RN_fupd f ∘ h)
⊦ ((∀n. 0 + n = n) ∧ (∀n. n + 0 = n) ∧ (∀n m. n + m = numeral.iZ (n + m)) ∧
(∀n. 0 * n = 0) ∧ (∀n. n * 0 = 0) ∧ (∀n m. n * m = n * m) ∧
(∀n. arithmetic.- 0 n = 0) ∧ (∀n. arithmetic.- n 0 = n) ∧
(∀n m. arithmetic.- n m = arithmetic.- n m) ∧ (∀n. 0 ↑ bit1 n = 0) ∧
(∀n. 0 ↑ arithmetic.BIT2 n = 0) ∧ (∀n. n ↑ 0 = 1) ∧
(∀n m. n ↑ m = n ↑ m) ∧ suc 0 = 1 ∧ (∀n. suc n = suc n) ∧
prim_rec.PRE 0 = 0 ∧ (∀n. prim_rec.PRE n = prim_rec.PRE n) ∧
(∀n. n = 0 ⇔ n = 0) ∧ (∀n. 0 = n ⇔ n = 0) ∧ (∀n m. n = m ⇔ n = m) ∧
(∀n. n < 0 ⇔ ⊥) ∧ (∀n. 0 < n ⇔ 0 < n) ∧ (∀n m. n < m ⇔ n < m) ∧
(∀n. 0 > n ⇔ ⊥) ∧ (∀n. n > 0 ⇔ 0 < n) ∧ (∀n m. n > m ⇔ m < n) ∧
(∀n. 0 ≤ n ⇔ ⊤) ∧ (∀n. n ≤ 0 ⇔ n ≤ 0) ∧ (∀n m. n ≤ m ⇔ n ≤ m) ∧
(∀n. n ≥ 0 ⇔ ⊤) ∧ (∀n. 0 ≥ n ⇔ n = 0) ∧ (∀n m. n ≥ m ⇔ m ≤ n) ∧
(∀n. odd n ⇔ odd n) ∧ (∀n. even n ⇔ even n) ∧ ¬odd 0 ∧ even 0) ∧
(∀n m.
(0 = bit1 n ⇔ ⊥) ∧ (bit1 n = 0 ⇔ ⊥) ∧ (0 = arithmetic.BIT2 n ⇔ ⊥) ∧
(arithmetic.BIT2 n = 0 ⇔ ⊥) ∧ (bit1 n = arithmetic.BIT2 m ⇔ ⊥) ∧
(arithmetic.BIT2 n = bit1 m ⇔ ⊥) ∧ (bit1 n = bit1 m ⇔ n = m) ∧
(arithmetic.BIT2 n = arithmetic.BIT2 m ⇔ n = m)) ∧
(suc 0 = 1 ∧ (∀n. suc (bit1 n) = arithmetic.BIT2 n) ∧
∀n. suc (arithmetic.BIT2 n) = bit1 (suc n)) ∧
(numeral.iiSUC 0 = arithmetic.BIT2 0 ∧
numeral.iiSUC (bit1 n) = bit1 (suc n) ∧
numeral.iiSUC (arithmetic.BIT2 n) = arithmetic.BIT2 (suc n)) ∧
(∀n m.
numeral.iZ (0 + n) = n ∧ numeral.iZ (n + 0) = n ∧
numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m)) ∧
numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m)) ∧
numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m)) ∧
numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
arithmetic.BIT2 (suc (n + m)) ∧ suc (0 + n) = suc n ∧
suc (n + 0) = suc n ∧ suc (bit1 n + bit1 m) = bit1 (suc (n + m)) ∧
suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m)) ∧
suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m)) ∧
suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (0 + n) = numeral.iiSUC n ∧
numeral.iiSUC (n + 0) = numeral.iiSUC n ∧
numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m)) ∧
numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
arithmetic.BIT2 (numeral.iiSUC (n + m))) ∧
(∀n m.
0 * n = 0 ∧ n * 0 = 0 ∧
bit1 n * m = numeral.iZ (numeral.iDUB (n * m) + m) ∧
arithmetic.BIT2 n * m = numeral.iDUB (numeral.iZ (n * m + m))) ∧
(∀n.
numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n) ∧
numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n) ∧
numeral.iDUB 0 = 0) ∧ (0 = 0 ⇔ ⊤) ∧ (0 = 0 ⇔ ⊤)
⊦ semi_ring.is_semi_ring (semi_ring.recordtype.semi_ring 0 1 (+) (*)) ∧
(∀vm p.
numRing.num_interp_sp vm p =
numRing.num_interp_cs vm (numRing.num_spolynom_simplify p)) ∧
(((∀vm c. numRing.num_interp_sp vm (canonical.SPconst c) = c) ∧
(∀vm i.
numRing.num_interp_sp vm (canonical.SPvar i) =
quote.varmap_find i vm) ∧
(∀vm p1 p2.
numRing.num_interp_sp vm (canonical.SPplus p1 p2) =
numRing.num_interp_sp vm p1 + numRing.num_interp_sp vm p2) ∧
∀vm p1 p2.
numRing.num_interp_sp vm (canonical.SPmult p1 p2) =
numRing.num_interp_sp vm p1 * numRing.num_interp_sp vm p2) ∧
(∀x v2 v1.
quote.varmap_find quote.End_idx (quote.Node_vm x v1 v2) = x) ∧
(∀x v2 v1 i1.
quote.varmap_find (quote.Right_idx i1) (quote.Node_vm x v1 v2) =
quote.varmap_find i1 v2) ∧
(∀x v2 v1 i1.
quote.varmap_find (quote.Left_idx i1) (quote.Node_vm x v1 v2) =
quote.varmap_find i1 v1) ∧
∀i. quote.varmap_find i quote.Empty_vm = select x. ⊤) ∧
((∀t2 t1 l2 l1 c2 c1.
numRing.num_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
(canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1
(numRing.num_canonical_sum_merge t1
(canonical.Cons_monom c2 l2 t2)))
(canonical.Cons_monom (c1 + c2) l1
(numRing.num_canonical_sum_merge t1 t2))
(canonical.Cons_monom c2 l2
(numRing.num_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
t2))) ∧
(∀t2 t1 l2 l1 c1.
numRing.num_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
(canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1
(numRing.num_canonical_sum_merge t1
(canonical.Cons_varlist l2 t2)))
(canonical.Cons_monom (c1 + 1) l1
(numRing.num_canonical_sum_merge t1 t2))
(canonical.Cons_varlist l2
(numRing.num_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
t2))) ∧
(∀t2 t1 l2 l1 c2.
numRing.num_canonical_sum_merge (canonical.Cons_varlist l1 t1)
(canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1
(numRing.num_canonical_sum_merge t1
(canonical.Cons_monom c2 l2 t2)))
(canonical.Cons_monom (1 + c2) l1
(numRing.num_canonical_sum_merge t1 t2))
(canonical.Cons_monom c2 l2
(numRing.num_canonical_sum_merge (canonical.Cons_varlist l1 t1)
t2))) ∧
(∀t2 t1 l2 l1.
numRing.num_canonical_sum_merge (canonical.Cons_varlist l1 t1)
(canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1
(numRing.num_canonical_sum_merge t1
(canonical.Cons_varlist l2 t2)))
(canonical.Cons_monom (1 + 1) l1
(numRing.num_canonical_sum_merge t1 t2))
(canonical.Cons_varlist l2
(numRing.num_canonical_sum_merge (canonical.Cons_varlist l1 t1)
t2))) ∧
(∀s1. numRing.num_canonical_sum_merge s1 canonical.Nil_monom = s1) ∧
(∀v6 v5 v4.
numRing.num_canonical_sum_merge canonical.Nil_monom
(canonical.Cons_monom v4 v5 v6) = canonical.Cons_monom v4 v5 v6) ∧
∀v8 v7.
numRing.num_canonical_sum_merge canonical.Nil_monom
(canonical.Cons_varlist v7 v8) = canonical.Cons_varlist v7 v8) ∧
((∀t2 l2 l1 c2 c1.
numRing.num_monom_insert c1 l1 (canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1 (canonical.Cons_monom c2 l2 t2))
(canonical.Cons_monom (c1 + c2) l1 t2)
(canonical.Cons_monom c2 l2 (numRing.num_monom_insert c1 l1 t2))) ∧
(∀t2 l2 l1 c1.
numRing.num_monom_insert c1 l1 (canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_monom c1 l1 (canonical.Cons_varlist l2 t2))
(canonical.Cons_monom (c1 + 1) l1 t2)
(canonical.Cons_varlist l2 (numRing.num_monom_insert c1 l1 t2))) ∧
∀l1 c1.
numRing.num_monom_insert c1 l1 canonical.Nil_monom =
canonical.Cons_monom c1 l1 canonical.Nil_monom) ∧
((∀t2 l2 l1 c2.
numRing.num_varlist_insert l1 (canonical.Cons_monom c2 l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1 (canonical.Cons_monom c2 l2 t2))
(canonical.Cons_monom (1 + c2) l1 t2)
(canonical.Cons_monom c2 l2 (numRing.num_varlist_insert l1 t2))) ∧
(∀t2 l2 l1.
numRing.num_varlist_insert l1 (canonical.Cons_varlist l2 t2) =
prelim.compare (prelim.list_compare quote.index_compare l1 l2)
(canonical.Cons_varlist l1 (canonical.Cons_varlist l2 t2))
(canonical.Cons_monom (1 + 1) l1 t2)
(canonical.Cons_varlist l2 (numRing.num_varlist_insert l1 t2))) ∧
∀l1.
numRing.num_varlist_insert l1 canonical.Nil_monom =
canonical.Cons_varlist l1 canonical.Nil_monom) ∧
((∀c0 c l t.
numRing.num_canonical_sum_scalar c0 (canonical.Cons_monom c l t) =
canonical.Cons_monom (c0 * c) l
(numRing.num_canonical_sum_scalar c0 t)) ∧
(∀c0 l t.
numRing.num_canonical_sum_scalar c0 (canonical.Cons_varlist l t) =
canonical.Cons_monom c0 l (numRing.num_canonical_sum_scalar c0 t)) ∧
∀c0.
numRing.num_canonical_sum_scalar c0 canonical.Nil_monom =
canonical.Nil_monom) ∧
((∀l0 c l t.
numRing.num_canonical_sum_scalar2 l0 (canonical.Cons_monom c l t) =
numRing.num_monom_insert c (prelim.list_merge quote.index_lt l0 l)
(numRing.num_canonical_sum_scalar2 l0 t)) ∧
(∀l0 l t.
numRing.num_canonical_sum_scalar2 l0 (canonical.Cons_varlist l t) =
numRing.num_varlist_insert (prelim.list_merge quote.index_lt l0 l)
(numRing.num_canonical_sum_scalar2 l0 t)) ∧
∀l0.
numRing.num_canonical_sum_scalar2 l0 canonical.Nil_monom =
canonical.Nil_monom) ∧
((∀c0 l0 c l t.
numRing.num_canonical_sum_scalar3 c0 l0
(canonical.Cons_monom c l t) =
numRing.num_monom_insert (c0 * c)
(prelim.list_merge quote.index_lt l0 l)
(numRing.num_canonical_sum_scalar3 c0 l0 t)) ∧
(∀c0 l0 l t.
numRing.num_canonical_sum_scalar3 c0 l0
(canonical.Cons_varlist l t) =
numRing.num_monom_insert c0 (prelim.list_merge quote.index_lt l0 l)
(numRing.num_canonical_sum_scalar3 c0 l0 t)) ∧
∀c0 l0.
numRing.num_canonical_sum_scalar3 c0 l0 canonical.Nil_monom =
canonical.Nil_monom) ∧
((∀c1 l1 t1 s2.
numRing.num_canonical_sum_prod (canonical.Cons_monom c1 l1 t1) s2 =
numRing.num_canonical_sum_merge
(numRing.num_canonical_sum_scalar3 c1 l1 s2)
(numRing.num_canonical_sum_prod t1 s2)) ∧
(∀l1 t1 s2.
numRing.num_canonical_sum_prod (canonical.Cons_varlist l1 t1) s2 =
numRing.num_canonical_sum_merge
(numRing.num_canonical_sum_scalar2 l1 s2)
(numRing.num_canonical_sum_prod t1 s2)) ∧
∀s2.
numRing.num_canonical_sum_prod canonical.Nil_monom s2 =
canonical.Nil_monom) ∧
((∀c l t.
numRing.num_canonical_sum_simplify (canonical.Cons_monom c l t) =
if c = 0 then numRing.num_canonical_sum_simplify t
else if c = 1 then
canonical.Cons_varlist l (numRing.num_canonical_sum_simplify t)
else
canonical.Cons_monom c l (numRing.num_canonical_sum_simplify t)) ∧
(∀l t.
numRing.num_canonical_sum_simplify (canonical.Cons_varlist l t) =
canonical.Cons_varlist l (numRing.num_canonical_sum_simplify t)) ∧
numRing.num_canonical_sum_simplify canonical.Nil_monom =
canonical.Nil_monom) ∧
((∀vm x. numRing.num_ivl_aux vm x [] = quote.varmap_find x vm) ∧
∀vm x x' t'.
numRing.num_ivl_aux vm x (x' :: t') =
quote.varmap_find x vm * numRing.num_ivl_aux vm x' t') ∧
((∀vm. numRing.num_interp_vl vm [] = 1) ∧
∀vm x t.
numRing.num_interp_vl vm (x :: t) = numRing.num_ivl_aux vm x t) ∧
((∀vm c. numRing.num_interp_m vm c [] = c) ∧
∀vm c x t.
numRing.num_interp_m vm c (x :: t) = c * numRing.num_ivl_aux vm x t) ∧
((∀vm a. numRing.num_ics_aux vm a canonical.Nil_monom = a) ∧
(∀vm a l t.
numRing.num_ics_aux vm a (canonical.Cons_varlist l t) =
a + numRing.num_ics_aux vm (numRing.num_interp_vl vm l) t) ∧
∀vm a c l t.
numRing.num_ics_aux vm a (canonical.Cons_monom c l t) =
a + numRing.num_ics_aux vm (numRing.num_interp_m vm c l) t) ∧
((∀vm. numRing.num_interp_cs vm canonical.Nil_monom = 0) ∧
(∀vm l t.
numRing.num_interp_cs vm (canonical.Cons_varlist l t) =
numRing.num_ics_aux vm (numRing.num_interp_vl vm l) t) ∧
∀vm c l t.
numRing.num_interp_cs vm (canonical.Cons_monom c l t) =
numRing.num_ics_aux vm (numRing.num_interp_m vm c l) t) ∧
((∀i.
numRing.num_spolynom_normalize (canonical.SPvar i) =
canonical.Cons_varlist (i :: []) canonical.Nil_monom) ∧
(∀c.
numRing.num_spolynom_normalize (canonical.SPconst c) =
canonical.Cons_monom c [] canonical.Nil_monom) ∧
(∀l r.
numRing.num_spolynom_normalize (canonical.SPplus l r) =
numRing.num_canonical_sum_merge (numRing.num_spolynom_normalize l)
(numRing.num_spolynom_normalize r)) ∧
∀l r.
numRing.num_spolynom_normalize (canonical.SPmult l r) =
numRing.num_canonical_sum_prod (numRing.num_spolynom_normalize l)
(numRing.num_spolynom_normalize r)) ∧
∀x.
numRing.num_spolynom_simplify x =
numRing.num_canonical_sum_simplify (numRing.num_spolynom_normalize x)
External Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- List
- HOL4
- ind_type
- ind_type.recspace
- ind_type
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- []
- Pair
- ,
- fst
- snd
- Bool
- Function
- const
- id
- ∘
- HOL4
- arithmetic
- arithmetic.-
- arithmetic.BIT2
- bool
- bool.ARB
- bool.LET
- bool.TYPE_DEFINITION
- ind_type
- ind_type.BOTTOM
- ind_type.CONSTR
- ind_type.FCONS
- list
- list.list_CASE
- list.list_size
- numeral
- numeral.iDUB
- numeral.iSUB
- numeral.iZ
- numeral.iiSUC
- pair
- pair.pair_CASE
- pair.UNCURRY
- prim_rec
- prim_rec.PRE
- relation
- relation.inv_image
- relation.RESTRICT
- relation.WFREC
- arithmetic
- Number
- Natural
- *
- +
- <
- ≤
- >
- ≥
- ↑
- bit1
- even
- odd
- suc
- zero
- Natural
- Relation
- wellFounded
Assumptions
⊦ ⊤
⊦ wellFounded (<)
⊦ ∀t. ⊥ ⇒ t
⊦ ∀n. 0 ≤ n
⊦ bool.LET = λf x. f x
⊦ ∀x. id x = x
⊦ ∀t. t ∨ ¬t
⊦ (¬) = λt. t ⇒ ⊥
⊦ (∃) = λP. P ((select) P)
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λP. P = λx. ⊤
⊦ ∀x. x = x ⇔ ⊤
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀n. n * 0 = 0
⊦ ∀n. n + 0 = n
⊦ ∀A. A ⇒ ¬A ⇒ ⊥
⊦ ∀t. ¬t ⇒ t ⇒ ⊥
⊦ ∀t. (t ⇒ ⊥) ⇒ ¬t
⊦ ∀x y. const x y = x
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. t ⇒ ⊥ ⇔ t ⇔ ⊥
⊦ ∀n. suc n = 1 + n
⊦ ∀x. (fst x, snd x) = x
⊦ ∀x y. fst (x, y) = x
⊦ ∀x y. snd (x, y) = y
⊦ ∀a1 a0. ¬([] = a0 :: a1)
⊦ ∀P x. P x ⇒ P ((select) P)
⊦ pair.pair_CASE (x, y) f = f x y
⊦ ∀x. ∃q r. x = (q, r)
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀A B. A ∨ B ⇔ B ∨ A
⊦ ∀m n. m * n = n * m
⊦ ∀m n. m + n = n + m
⊦ ∀R f. wellFounded R ⇒ wellFounded (relation.inv_image R f)
⊦ (¬A ⇒ ⊥) ⇒ (A ⇒ ⊥) ⇒ ⊥
⊦ ∀m n. m < n ⇔ suc m ≤ n
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀P. ¬(∀m. P m) ⇔ ∃m. ¬P m
⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀R f. relation.inv_image R f = λx y. R (f x) (f y)
⊦ ∀l. l = [] ∨ ∃h t. l = h :: t
⊦ ∀P a. (∃a0''. a0'' = a ∧ P a0'') ⇔ P a
⊦ ∀P t. (∀x. x = t ⇒ P x) ⇒ (∃) P
⊦ ∀f x y. pair.UNCURRY f (x, y) = f x y
⊦ (∨) = λt1 t2. ∀t. (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t
⊦ ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)
⊦ ∀m n. m = n ⇔ m ≤ n ∧ n ≤ m
⊦ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)
⊦ ¬(¬A ∨ B) ⇒ ⊥ ⇔ A ⇒ ¬B ⇒ ⊥
⊦ ∀P Q. P ∨ (∃x. Q x) ⇔ ∃x. P ∨ Q x
⊦ ∀P Q. (∃x. P x ∧ Q) ⇔ (∃x. P x) ∧ Q
⊦ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q
⊦ ¬(A ∨ B) ⇒ ⊥ ⇔ (A ⇒ ⊥) ⇒ ¬B ⇒ ⊥
⊦ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∧ z ⇒ y ∧ w
⊦ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∨ z ⇒ y ∨ w
⊦ ∀x y z. x = y ∧ y = z ⇒ x = z
⊦ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3
⊦ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3
⊦ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C
⊦ ∀m n p. m * (n * p) = m * n * p
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀m n p. m + p = n + p ⇔ m = n
⊦ ∀m n p. m + p < n + p ⇔ m < n
⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀f g h. f ∘ (g ∘ h) = f ∘ g ∘ h
⊦ (∀x. P x ⇒ Q x) ⇒ (∃x. P x) ⇒ ∃x. Q x
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1 ∧ (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (t1 ⇔ t2) ⇔ t1 ∧ t2 ∨ ¬t1 ∧ ¬t2
⊦ ∀n m. arithmetic.- n m = if m < n then numeral.iSUB ⊤ n m else 0
⊦ (∀t. ¬¬t ⇔ t) ∧ (¬⊤ ⇔ ⊥) ∧ (¬⊥ ⇔ ⊤)
⊦ ∀m n. ¬(m = n) ⇔ suc m ≤ n ∨ suc n ≤ m
⊦ ∀m n p. (m + n) * p = m * p + n * p
⊦ ∀f R y z. R y z ⇒ relation.RESTRICT f R z y = f y
⊦ ∀P Q. (∃x. P x ∨ Q x) ⇔ (∃x. P x) ∨ ∃x. Q x
⊦ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h :: t)) ⇒ ∀l1. P l1
⊦ ∀a0 a1 a0' a1'. a0 :: a1 = a0' :: a1' ⇔ a0 = a0' ∧ a1 = a1'
⊦ ∀Fn. ∃f. ∀c i r. f (ind_type.CONSTR c i r) = Fn c i r (λn. f (r n))
⊦ numeral.iiSUC 0 = arithmetic.BIT2 0 ∧
numeral.iiSUC (bit1 n) = bit1 (suc n) ∧
numeral.iiSUC (arithmetic.BIT2 n) = arithmetic.BIT2 (suc n)
⊦ ∀n.
numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n) ∧
numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n) ∧
numeral.iDUB 0 = 0
⊦ (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)
⊦ (p ⇔ q ∨ r) ⇔ (p ∨ ¬q) ∧ (p ∨ ¬r) ∧ (q ∨ r ∨ ¬p)
⊦ ∀f0 f1. ∃fn. fn [] = f0 ∧ ∀a0 a1. fn (a0 :: a1) = f1 a0 a1 (fn a1)
⊦ ∀R. wellFounded R ⇒ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x
⊦ (∀a f. ind_type.FCONS a f 0 = a) ∧
∀a f n. ind_type.FCONS a f (suc n) = f n
⊦ ∀x x' y y'. (x ⇔ x') ∧ (x' ⇒ (y ⇔ y')) ⇒ (x ⇒ y ⇔ x' ⇒ y')
⊦ (p ⇔ q ∧ r) ⇔ (p ∨ ¬q ∨ ¬r) ∧ (q ∨ ¬p) ∧ (r ∨ ¬p)
⊦ suc 0 = 1 ∧ (∀n. suc (bit1 n) = arithmetic.BIT2 n) ∧
∀n. suc (arithmetic.BIT2 n) = bit1 (suc n)
⊦ P (arithmetic.- a b) ⇔ ∀d. (b = a + d ⇒ P 0) ∧ (a = b + d ⇒ P d)
⊦ ∀A B. (¬(A ∧ B) ⇔ ¬A ∨ ¬B) ∧ (¬(A ∨ B) ⇔ ¬A ∧ ¬B)
⊦ ∀M R f.
f = relation.WFREC R M ⇒ wellFounded R ⇒
∀x. f x = M (relation.RESTRICT f R x) x
⊦ bool.TYPE_DEFINITION =
λP rep.
(∀x' x''. rep x' = rep x'' ⇒ x' = x'') ∧ ∀x. P x ⇔ ∃x'. x = rep x'
⊦ (∀v f. list.list_CASE [] v f = v) ∧
∀a0 a1 v f. list.list_CASE (a0 :: a1) v f = f a0 a1
⊦ ∀t. ((⊤ ⇔ t) ⇔ t) ∧ ((t ⇔ ⊤) ⇔ t) ∧ ((⊥ ⇔ t) ⇔ ¬t) ∧ ((t ⇔ ⊥) ⇔ ¬t)
⊦ ∀P.
(∃rep. bool.TYPE_DEFINITION P rep) ⇒
∃rep abs. (∀a. abs (rep a) = a) ∧ ∀r. P r ⇔ rep (abs r) = r
⊦ (∀f. list.list_size f [] = 0) ∧
∀f a0 a1. list.list_size f (a0 :: a1) = 1 + (f a0 + list.list_size f a1)
⊦ ∀t. (⊤ ∧ t ⇔ t) ∧ (t ∧ ⊤ ⇔ t) ∧ (⊥ ∧ t ⇔ ⊥) ∧ (t ∧ ⊥ ⇔ ⊥) ∧ (t ∧ t ⇔ t)
⊦ ∀t. (⊤ ∨ t ⇔ ⊤) ∧ (t ∨ ⊤ ⇔ ⊤) ∧ (⊥ ∨ t ⇔ t) ∧ (t ∨ ⊥ ⇔ t) ∧ (t ∨ t ⇔ t)
⊦ ∀t. (⊤ ⇒ t ⇔ t) ∧ (t ⇒ ⊤ ⇔ ⊤) ∧ (⊥ ⇒ t ⇔ ⊤) ∧ (t ⇒ t ⇔ ⊤) ∧ (t ⇒ ⊥ ⇔ ¬t)
⊦ ∀P Q x x' y y'.
(P ⇔ Q) ∧ (Q ⇒ x = x') ∧ (¬Q ⇒ y = y') ⇒
(if P then x else y) = if Q then x' else y'
⊦ (p ⇔ q ⇔ r) ⇔ (p ∨ q ∨ r) ∧ (p ∨ ¬r ∨ ¬q) ∧ (q ∨ ¬r ∨ ¬p) ∧ (r ∨ ¬q ∨ ¬p)
⊦ ∀n m.
0 * n = 0 ∧ n * 0 = 0 ∧
bit1 n * m = numeral.iZ (numeral.iDUB (n * m) + m) ∧
arithmetic.BIT2 n * m = numeral.iDUB (numeral.iZ (n * m + m))
⊦ ∀m n.
0 * m = 0 ∧ m * 0 = 0 ∧ 1 * m = m ∧ m * 1 = m ∧ suc m * n = m * n + n ∧
m * suc n = m + m * n
⊦ ∀n m.
(0 ≤ n ⇔ ⊤) ∧ (bit1 n ≤ 0 ⇔ ⊥) ∧ (arithmetic.BIT2 n ≤ 0 ⇔ ⊥) ∧
(bit1 n ≤ bit1 m ⇔ n ≤ m) ∧ (bit1 n ≤ arithmetic.BIT2 m ⇔ n ≤ m) ∧
(arithmetic.BIT2 n ≤ bit1 m ⇔ ¬(m ≤ n)) ∧
(arithmetic.BIT2 n ≤ arithmetic.BIT2 m ⇔ n ≤ m)
⊦ ∀n m.
(0 < bit1 n ⇔ ⊤) ∧ (0 < arithmetic.BIT2 n ⇔ ⊤) ∧ (n < 0 ⇔ ⊥) ∧
(bit1 n < bit1 m ⇔ n < m) ∧
(arithmetic.BIT2 n < arithmetic.BIT2 m ⇔ n < m) ∧
(bit1 n < arithmetic.BIT2 m ⇔ ¬(m < n)) ∧
(arithmetic.BIT2 n < bit1 m ⇔ n < m)
⊦ ∀n m.
(0 = bit1 n ⇔ ⊥) ∧ (bit1 n = 0 ⇔ ⊥) ∧ (0 = arithmetic.BIT2 n ⇔ ⊥) ∧
(arithmetic.BIT2 n = 0 ⇔ ⊥) ∧ (bit1 n = arithmetic.BIT2 m ⇔ ⊥) ∧
(arithmetic.BIT2 n = bit1 m ⇔ ⊥) ∧ (bit1 n = bit1 m ⇔ n = m) ∧
(arithmetic.BIT2 n = arithmetic.BIT2 m ⇔ n = m)
⊦ ∀b n m.
numeral.iSUB b 0 x = 0 ∧ numeral.iSUB ⊤ n 0 = n ∧
numeral.iSUB ⊥ (bit1 n) 0 = numeral.iDUB n ∧
numeral.iSUB ⊤ (bit1 n) (bit1 m) = numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (bit1 n) (bit1 m) = bit1 (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊤ (bit1 n) (arithmetic.BIT2 m) =
bit1 (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊥ (bit1 n) (arithmetic.BIT2 m) =
numeral.iDUB (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) 0 = bit1 n ∧
numeral.iSUB ⊤ (arithmetic.BIT2 n) (bit1 m) =
bit1 (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) (bit1 m) =
numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊤ (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
bit1 (numeral.iSUB ⊥ n m)
⊦ ∀n m.
numeral.iZ (0 + n) = n ∧ numeral.iZ (n + 0) = n ∧
numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m)) ∧
numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m)) ∧
numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m)) ∧
numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
arithmetic.BIT2 (suc (n + m)) ∧ suc (0 + n) = suc n ∧
suc (n + 0) = suc n ∧ suc (bit1 n + bit1 m) = bit1 (suc (n + m)) ∧
suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m)) ∧
suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m)) ∧
suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (0 + n) = numeral.iiSUC n ∧
numeral.iiSUC (n + 0) = numeral.iiSUC n ∧
numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m)) ∧
numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
arithmetic.BIT2 (numeral.iiSUC (n + m))
⊦ (∀n. 0 + n = n) ∧ (∀n. n + 0 = n) ∧ (∀n m. n + m = numeral.iZ (n + m)) ∧
(∀n. 0 * n = 0) ∧ (∀n. n * 0 = 0) ∧ (∀n m. n * m = n * m) ∧
(∀n. arithmetic.- 0 n = 0) ∧ (∀n. arithmetic.- n 0 = n) ∧
(∀n m. arithmetic.- n m = arithmetic.- n m) ∧ (∀n. 0 ↑ bit1 n = 0) ∧
(∀n. 0 ↑ arithmetic.BIT2 n = 0) ∧ (∀n. n ↑ 0 = 1) ∧
(∀n m. n ↑ m = n ↑ m) ∧ suc 0 = 1 ∧ (∀n. suc n = suc n) ∧
prim_rec.PRE 0 = 0 ∧ (∀n. prim_rec.PRE n = prim_rec.PRE n) ∧
(∀n. n = 0 ⇔ n = 0) ∧ (∀n. 0 = n ⇔ n = 0) ∧ (∀n m. n = m ⇔ n = m) ∧
(∀n. n < 0 ⇔ ⊥) ∧ (∀n. 0 < n ⇔ 0 < n) ∧ (∀n m. n < m ⇔ n < m) ∧
(∀n. 0 > n ⇔ ⊥) ∧ (∀n. n > 0 ⇔ 0 < n) ∧ (∀n m. n > m ⇔ m < n) ∧
(∀n. 0 ≤ n ⇔ ⊤) ∧ (∀n. n ≤ 0 ⇔ n ≤ 0) ∧ (∀n m. n ≤ m ⇔ n ≤ m) ∧
(∀n. n ≥ 0 ⇔ ⊤) ∧ (∀n. 0 ≥ n ⇔ n = 0) ∧ (∀n m. n ≥ m ⇔ m ≤ n) ∧
(∀n. odd n ⇔ odd n) ∧ (∀n. even n ⇔ even n) ∧ ¬odd 0 ∧ even 0