- semi_ring_TY_DEF
-
|- ∃rep.
TYPE_DEFINITION
(λa0'.
∀'semi_ring' .
(∀a0'.
(∃a0 a1 a2 a3.
a0' =
(λa0 a1 a2 a3.
ind_type$CONSTR 0 (a0,a1,a2,a3) (λn. ind_type$BOTTOM)) a0
a1 a2 a3) ⇒
'semi_ring' a0') ⇒
'semi_ring' a0') rep
- semi_ring_case_def
-
|- ∀a0 a1 a2 a3 f. semi_ring_CASE (semi_ring a0 a1 a2 a3) f = f a0 a1 a2 a3
- semi_ring_size_def
-
|- ∀f a0 a1 a2 a3.
semi_ring_size f (semi_ring a0 a1 a2 a3) = 1 + (f a0 + f a1)
- semi_ring_SR0
-
|- ∀a a0 f f0. SR0 (semi_ring a a0 f f0) = a
- semi_ring_SR1
-
|- ∀a a0 f f0. SR1 (semi_ring a a0 f f0) = a0
- semi_ring_SRP
-
|- ∀a a0 f f0. SRP (semi_ring a a0 f f0) = f
- semi_ring_SRM
-
|- ∀a a0 f f0. SRM (semi_ring a a0 f f0) = f0
- semi_ring_SR0_fupd
-
|- ∀f1 a a0 f f0.
semi_ring a a0 f f0 with SR0 updated_by f1 = semi_ring (f1 a) a0 f f0
- semi_ring_SR1_fupd
-
|- ∀f1 a a0 f f0.
semi_ring a a0 f f0 with SR1 updated_by f1 = semi_ring a (f1 a0) f f0
- semi_ring_SRP_fupd
-
|- ∀f1 a a0 f f0.
semi_ring a a0 f f0 with SRP updated_by f1 = semi_ring a a0 (f1 f) f0
- semi_ring_SRM_fupd
-
|- ∀f1 a a0 f f0.
semi_ring a a0 f f0 with SRM updated_by f1 = semi_ring a a0 f (f1 f0)
- is_semi_ring_def
-
|- ∀r.
is_semi_ring r ⇔
(∀n m. SRP r n m = SRP r m n) ∧
(∀n m p. SRP r n (SRP r m p) = SRP r (SRP r n m) p) ∧
(∀n m. SRM r n m = SRM r m n) ∧
(∀n m p. SRM r n (SRM r m p) = SRM r (SRM r n m) p) ∧
(∀n. SRP r (SR0 r) n = n) ∧ (∀n. SRM r (SR1 r) n = n) ∧
(∀n. SRM r (SR0 r) n = SR0 r) ∧
∀n m p. SRM r (SRP r n m) p = SRP r (SRM r n p) (SRM r m p)
- semi_ring_accessors
-
|- (∀a a0 f f0. SR0 (semi_ring a a0 f f0) = a) ∧
(∀a a0 f f0. SR1 (semi_ring a a0 f f0) = a0) ∧
(∀a a0 f f0. SRP (semi_ring a a0 f f0) = f) ∧
∀a a0 f f0. SRM (semi_ring a a0 f f0) = f0
- semi_ring_fn_updates
-
|- (∀f1 a a0 f f0.
semi_ring a a0 f f0 with SR0 updated_by f1 = semi_ring (f1 a) a0 f f0) ∧
(∀f1 a a0 f f0.
semi_ring a a0 f f0 with SR1 updated_by f1 = semi_ring a (f1 a0) f f0) ∧
(∀f1 a a0 f f0.
semi_ring a a0 f f0 with SRP updated_by f1 = semi_ring a a0 (f1 f) f0) ∧
∀f1 a a0 f f0.
semi_ring a a0 f f0 with SRM updated_by f1 = semi_ring a a0 f (f1 f0)
- semi_ring_accfupds
-
|- (∀s f. SR0 (s with SR1 updated_by f) = SR0 s) ∧
(∀s f. SR0 (s with SRP updated_by f) = SR0 s) ∧
(∀s f. SR0 (s with SRM updated_by f) = SR0 s) ∧
(∀s f. SR1 (s with SR0 updated_by f) = SR1 s) ∧
(∀s f. SR1 (s with SRP updated_by f) = SR1 s) ∧
(∀s f. SR1 (s with SRM updated_by f) = SR1 s) ∧
(∀s f. SRP (s with SR0 updated_by f) = SRP s) ∧
(∀s f. SRP (s with SR1 updated_by f) = SRP s) ∧
(∀s f. SRP (s with SRM updated_by f) = SRP s) ∧
(∀s f. SRM (s with SR0 updated_by f) = SRM s) ∧
(∀s f. SRM (s with SR1 updated_by f) = SRM s) ∧
(∀s f. SRM (s with SRP updated_by f) = SRM s) ∧
(∀s f. SR0 (s with SR0 updated_by f) = f (SR0 s)) ∧
(∀s f. SR1 (s with SR1 updated_by f) = f (SR1 s)) ∧
(∀s f. SRP (s with SRP updated_by f) = f (SRP s)) ∧
∀s f. SRM (s with SRM updated_by f) = f (SRM s)
- semi_ring_fupdfupds
-
|- (∀s g f.
s with <|SR0 updated_by f; SR0 updated_by g|> =
s with SR0 updated_by f o g) ∧
(∀s g f.
s with <|SR1 updated_by f; SR1 updated_by g|> =
s with SR1 updated_by f o g) ∧
(∀s g f.
s with <|SRP updated_by f; SRP updated_by g|> =
s with SRP updated_by f o g) ∧
∀s g f.
s with <|SRM updated_by f; SRM updated_by g|> =
s with SRM updated_by f o g
- semi_ring_fupdfupds_comp
-
|- ((∀g f.
_ record fupdateSR0 f o _ record fupdateSR0 g =
_ record fupdateSR0 (f o g)) ∧
∀h g f.
_ record fupdateSR0 f o _ record fupdateSR0 g o h =
_ record fupdateSR0 (f o g) o h) ∧
((∀g f.
_ record fupdateSR1 f o _ record fupdateSR1 g =
_ record fupdateSR1 (f o g)) ∧
∀h g f.
_ record fupdateSR1 f o _ record fupdateSR1 g o h =
_ record fupdateSR1 (f o g) o h) ∧
((∀g f.
_ record fupdateSRP f o _ record fupdateSRP g =
_ record fupdateSRP (f o g)) ∧
∀h g f.
_ record fupdateSRP f o _ record fupdateSRP g o h =
_ record fupdateSRP (f o g) o h) ∧
(∀g f.
_ record fupdateSRM f o _ record fupdateSRM g =
_ record fupdateSRM (f o g)) ∧
∀h g f.
_ record fupdateSRM f o _ record fupdateSRM g o h =
_ record fupdateSRM (f o g) o h
- semi_ring_fupdcanon
-
|- (∀s g f.
s with <|SR1 updated_by f; SR0 updated_by g|> =
s with <|SR0 updated_by g; SR1 updated_by f|>) ∧
(∀s g f.
s with <|SRP updated_by f; SR0 updated_by g|> =
s with <|SR0 updated_by g; SRP updated_by f|>) ∧
(∀s g f.
s with <|SRP updated_by f; SR1 updated_by g|> =
s with <|SR1 updated_by g; SRP updated_by f|>) ∧
(∀s g f.
s with <|SRM updated_by f; SR0 updated_by g|> =
s with <|SR0 updated_by g; SRM updated_by f|>) ∧
(∀s g f.
s with <|SRM updated_by f; SR1 updated_by g|> =
s with <|SR1 updated_by g; SRM updated_by f|>) ∧
∀s g f.
s with <|SRM updated_by f; SRP updated_by g|> =
s with <|SRP updated_by g; SRM updated_by f|>
- semi_ring_fupdcanon_comp
-
|- ((∀g f.
_ record fupdateSR1 f o _ record fupdateSR0 g =
_ record fupdateSR0 g o _ record fupdateSR1 f) ∧
∀h g f.
_ record fupdateSR1 f o _ record fupdateSR0 g o h =
_ record fupdateSR0 g o _ record fupdateSR1 f o h) ∧
((∀g f.
_ record fupdateSRP f o _ record fupdateSR0 g =
_ record fupdateSR0 g o _ record fupdateSRP f) ∧
∀h g f.
_ record fupdateSRP f o _ record fupdateSR0 g o h =
_ record fupdateSR0 g o _ record fupdateSRP f o h) ∧
((∀g f.
_ record fupdateSRP f o _ record fupdateSR1 g =
_ record fupdateSR1 g o _ record fupdateSRP f) ∧
∀h g f.
_ record fupdateSRP f o _ record fupdateSR1 g o h =
_ record fupdateSR1 g o _ record fupdateSRP f o h) ∧
((∀g f.
_ record fupdateSRM f o _ record fupdateSR0 g =
_ record fupdateSR0 g o _ record fupdateSRM f) ∧
∀h g f.
_ record fupdateSRM f o _ record fupdateSR0 g o h =
_ record fupdateSR0 g o _ record fupdateSRM f o h) ∧
((∀g f.
_ record fupdateSRM f o _ record fupdateSR1 g =
_ record fupdateSR1 g o _ record fupdateSRM f) ∧
∀h g f.
_ record fupdateSRM f o _ record fupdateSR1 g o h =
_ record fupdateSR1 g o _ record fupdateSRM f o h) ∧
(∀g f.
_ record fupdateSRM f o _ record fupdateSRP g =
_ record fupdateSRP g o _ record fupdateSRM f) ∧
∀h g f.
_ record fupdateSRM f o _ record fupdateSRP g o h =
_ record fupdateSRP g o _ record fupdateSRM f o h
- semi_ring_component_equality
-
|- ∀s1 s2.
(s1 = s2) ⇔
(SR0 s1 = SR0 s2) ∧ (SR1 s1 = SR1 s2) ∧ (SRP s1 = SRP s2) ∧
(SRM s1 = SRM s2)
- semi_ring_updates_eq_literal
-
|- ∀s a0 a f0 f.
s with <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|> =
<|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>
- semi_ring_literal_nchotomy
-
|- ∀s. ∃a0 a f0 f. s = <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>
- FORALL_semi_ring
-
|- ∀P. (∀s. P s) ⇔ ∀a0 a f0 f. P <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>
- EXISTS_semi_ring
-
|- ∀P. (∃s. P s) ⇔ ∃a0 a f0 f. P <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>
- semi_ring_literal_11
-
|- ∀a01 a1 f01 f1 a02 a2 f02 f2.
(<|SR0 := a01; SR1 := a1; SRP := f01; SRM := f1|> =
<|SR0 := a02; SR1 := a2; SRP := f02; SRM := f2|>) ⇔
(a01 = a02) ∧ (a1 = a2) ∧ (f01 = f02) ∧ (f1 = f2)
- datatype_semi_ring
-
|- DATATYPE (record semi_ring SR0 SR1 SRP SRM)
- semi_ring_11
-
|- ∀a0 a1 a2 a3 a0' a1' a2' a3'.
(semi_ring a0 a1 a2 a3 = semi_ring a0' a1' a2' a3') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2') ∧ (a3 = a3')
- semi_ring_case_cong
-
|- ∀M M' f.
(M = M') ∧
(∀a0 a1 a2 a3.
(M' = semi_ring a0 a1 a2 a3) ⇒ (f a0 a1 a2 a3 = f' a0 a1 a2 a3)) ⇒
(semi_ring_CASE M f = semi_ring_CASE M' f')
- semi_ring_nchotomy
-
|- ∀ss. ∃a a0 f f0. ss = semi_ring a a0 f f0
- semi_ring_Axiom
-
|- ∀f. ∃fn. ∀a0 a1 a2 a3. fn (semi_ring a0 a1 a2 a3) = f a0 a1 a2 a3
- semi_ring_induction
-
|- ∀P. (∀a a0 f f0. P (semi_ring a a0 f f0)) ⇒ ∀s. P s
- plus_sym
-
|- ∀r. is_semi_ring r ⇒ ∀n m. SRP r n m = SRP r m n
- plus_assoc
-
|- ∀r. is_semi_ring r ⇒ ∀n m p. SRP r n (SRP r m p) = SRP r (SRP r n m) p
- mult_sym
-
|- ∀r. is_semi_ring r ⇒ ∀n m. SRM r n m = SRM r m n
- mult_assoc
-
|- ∀r. is_semi_ring r ⇒ ∀n m p. SRM r n (SRM r m p) = SRM r (SRM r n m) p
- plus_zero_left
-
|- ∀r. is_semi_ring r ⇒ ∀n. SRP r (SR0 r) n = n
- mult_one_left
-
|- ∀r. is_semi_ring r ⇒ ∀n. SRM r (SR1 r) n = n
- mult_zero_left
-
|- ∀r. is_semi_ring r ⇒ ∀n. SRM r (SR0 r) n = SR0 r
- distr_left
-
|- ∀r.
is_semi_ring r ⇒
∀n m p. SRM r (SRP r n m) p = SRP r (SRM r n p) (SRM r m p)
- plus_zero_right
-
|- ∀r. is_semi_ring r ⇒ ∀n. SRP r n (SR0 r) = n
- mult_one_right
-
|- ∀r. is_semi_ring r ⇒ ∀n. SRM r n (SR1 r) = n
- mult_zero_right
-
|- ∀r. is_semi_ring r ⇒ ∀n. SRM r n (SR0 r) = SR0 r
- distr_right
-
|- ∀r.
is_semi_ring r ⇒
∀m n p. SRM r m (SRP r n p) = SRP r (SRM r m n) (SRM r m p)
- plus_rotate
-
|- ∀r. is_semi_ring r ⇒ ∀m n p. SRP r (SRP r m n) p = SRP r (SRP r n p) m
- plus_permute
-
|- ∀r. is_semi_ring r ⇒ ∀m n p. SRP r (SRP r m n) p = SRP r (SRP r m p) n
- mult_rotate
-
|- ∀r. is_semi_ring r ⇒ ∀m n p. SRM r (SRM r m n) p = SRM r (SRM r n p) m
- mult_permute
-
|- ∀r. is_semi_ring r ⇒ ∀m n p. SRM r (SRM r m n) p = SRM r (SRM r m p) n