Beginning of Section Alg
Variable extension_tag : set
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha extension_tag
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
Definition. We define
pair_tag to be
λx y ⇒ x ∪ {u ''|u ∈ y} of type
set → set → set.
Variable F : set → prop
Hypothesis extension_tag_fresh : ∀x, F x → ∀u ∈ x, extension_tag ∉ u
Axiom. (
ctagged_eqE_eq) We take the following as an axiom:
∀x y, F x → F y → ∀u ∈ x, ∀v ∈ y, u '' = v '' → u = v
Axiom. (
pair_tag_0) We take the following as an axiom:
Primitive. The name
CD_carr is a term of type
set → prop.
Axiom. (
CD_carr_I) We take the following as an axiom:
Axiom. (
CD_carr_E) We take the following as an axiom:
Definition. We define
CD_proj0 to be
λz ⇒ Eps_i (λx ⇒ F x ∧ ∃y, F y ∧ z = pair_tag x y) of type
set → set.
Axiom. (
CD_proj0_1) We take the following as an axiom:
∀z, CD_carr z → F (proj0 z) ∧ ∃y, F y ∧ z = pa (proj0 z) y
Axiom. (
CD_proj0_2) We take the following as an axiom:
∀x y, F x → F y → proj0 (pa x y) = x
Axiom. (
CD_proj1_1) We take the following as an axiom:
∀z, CD_carr z → F (proj1 z) ∧ z = pa (proj0 z) (proj1 z)
Axiom. (
CD_proj1_2) We take the following as an axiom:
∀x y, F x → F y → proj1 (pa x y) = y
Axiom. (
CD_proj0R) We take the following as an axiom:
Axiom. (
CD_proj1R) We take the following as an axiom:
Axiom. (
CD_proj0_F) We take the following as an axiom:
Axiom. (
CD_proj1_F) We take the following as an axiom:
Beginning of Section CD_minus_conj
Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Definition. We define
CD_minus to be
λz ⇒ pa (- proj0 z) (- proj1 z) of type
set → set.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus.
Variable conj : set → set
Definition. We define
CD_conj to be
λz ⇒ pa (conj (proj0 z)) (- proj1 z) of type
set → set.
End of Section CD_minus_conj
Beginning of Section CD_add
Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Definition. We define
CD_add to be
λz w ⇒ pa (proj0 z + proj0 w) (proj1 z + proj1 w) of type
set → set → set.
End of Section CD_add
Beginning of Section CD_mul
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Definition. We define
CD_mul to be
λz w ⇒ pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) of type
set → set → set.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul.
Definition. We define
CD_exp_nat to be
λz m ⇒ nat_primrec 1 (λ_ r ⇒ z ⨯ r) m of type
set → set → set.
End of Section CD_mul
Beginning of Section CD_minus_conj_clos
Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Hypothesis F_minus : ∀x, F x → F (- x)
Axiom. (
CD_minus_CD) We take the following as an axiom:
Variable conj : set → set
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Hypothesis F_conj : ∀x, F x → F (conj x)
Axiom. (
CD_conj_CD) We take the following as an axiom:
End of Section CD_minus_conj_clos
Beginning of Section CD_add_clos
Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Axiom. (
CD_add_CD) We take the following as an axiom:
End of Section CD_add_clos
Beginning of Section CD_mul_clos
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
Axiom. (
CD_mul_CD) We take the following as an axiom:
End of Section CD_mul_clos
Beginning of Section CD_minus_conj_F
Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Hypothesis F_0 : F 0
Hypothesis F_minus_0 : - 0 = 0
Variable conj : set → set
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
End of Section CD_minus_conj_F
Beginning of Section CD_add_F
Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_0 : F 0
Hypothesis F_add_0_0 : 0 + 0 = 0
Axiom. (
CD_add_F_eq) We take the following as an axiom:
∀x y, F x → F y → x + y = x + y
End of Section CD_add_F
Beginning of Section CD_mul_F
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_0 : F 0
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
Hypothesis F_minus_0 : - 0 = 0
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
Axiom. (
CD_mul_F_eq) We take the following as an axiom:
∀x y, F x → F y → x ⨯ y = x * y
End of Section CD_mul_F
Beginning of Section CD_minus_invol
Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_minus_invol : ∀x, F x → - - x = x
End of Section CD_minus_invol
Beginning of Section CD_conj_invol
Variable minus : set → set
Variable conj : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_minus_invol : ∀x, F x → - - x = x
Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x
End of Section CD_conj_invol
Beginning of Section CD_conj_minus
Variable minus : set → set
Variable conj : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
End of Section CD_conj_minus
Beginning of Section CD_minus_add
Variable minus : set → set
Variable add : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
End of Section CD_minus_add
Beginning of Section CD_conj_add
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
Axiom. (
CD_conj_add) We take the following as an axiom:
End of Section CD_conj_add
Beginning of Section CD_add_com
Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
Axiom. (
CD_add_com) We take the following as an axiom:
End of Section CD_add_com
Beginning of Section CD_add_assoc
Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
End of Section CD_add_assoc
Beginning of Section CD_add_0R
Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_0 : F 0
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
Axiom. (
CD_add_0R) We take the following as an axiom:
End of Section CD_add_0R
Beginning of Section CD_add_0L
Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_0 : F 0
Hypothesis F_add_0L : ∀x, F x → 0 + x = x
Axiom. (
CD_add_0L) We take the following as an axiom:
End of Section CD_add_0L
Beginning of Section CD_add_minus_linv
Variable minus : set → set
Variable add : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_add_minus_linv : ∀x, F x → - x + x = 0
End of Section CD_add_minus_linv
Beginning of Section CD_add_minus_rinv
Variable minus : set → set
Variable add : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_add_minus_rinv : ∀x, F x → x + - x = 0
End of Section CD_add_minus_rinv
Beginning of Section CD_mul_0R
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_0 : F 0
Hypothesis F_minus_0 : - 0 = 0
Hypothesis F_conj_0 : conj 0 = 0
Hypothesis F_add_0_0 : 0 + 0 = 0
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
Axiom. (
CD_mul_0R) We take the following as an axiom:
End of Section CD_mul_0R
Beginning of Section CD_mul_0L
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_0 : F 0
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_minus_0 : - 0 = 0
Hypothesis F_add_0_0 : 0 + 0 = 0
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
Axiom. (
CD_mul_0L) We take the following as an axiom:
End of Section CD_mul_0L
Beginning of Section CD_mul_1R
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_0 : F 0
Hypothesis F_1 : F 1
Hypothesis F_minus_0 : - 0 = 0
Hypothesis F_conj_0 : conj 0 = 0
Hypothesis F_conj_1 : conj 1 = 1
Hypothesis F_add_0L : ∀x, F x → 0 + x = x
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
Axiom. (
CD_mul_1R) We take the following as an axiom:
End of Section CD_mul_1R
Beginning of Section CD_mul_1L
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_0 : F 0
Hypothesis F_1 : F 1
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_minus_0 : - 0 = 0
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
Hypothesis F_mul_1L : ∀x, F x → 1 * x = x
Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
Axiom. (
CD_mul_1L) We take the following as an axiom:
End of Section CD_mul_1L
Beginning of Section CD_conj_mul
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
Hypothesis F_minus_invol : ∀x, F x → - - x = x
Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x
Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
Hypothesis F_conj_mul : ∀x y, F x → F y → conj (x * y) = conj y * conj x
Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
Axiom. (
CD_conj_mul) We take the following as an axiom:
End of Section CD_conj_mul
Beginning of Section CD_add_mul_distrR
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z
Hypothesis F_add_mul_distrR : ∀x y z, F x → F y → F z → (x + y) * z = x * z + y * z
End of Section CD_add_mul_distrR
Beginning of Section CD_add_mul_distrL
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z
Hypothesis F_add_mul_distrR : ∀x y z, F x → F y → F z → (x + y) * z = x * z + y * z
End of Section CD_add_mul_distrL
Beginning of Section CD_minus_mul_distrR
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
End of Section CD_minus_mul_distrR
Beginning of Section CD_minus_mul_distrL
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
End of Section CD_minus_mul_distrL
Beginning of Section CD_exp_nat
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Notation. We use
^ as an infix operator with priority 342 and no associativity corresponding to applying term
CD_exp_nat minus conj add mul.
Axiom. (
CD_exp_nat_S) We take the following as an axiom:
∀z n, nat_p n → z ^ (ordsucc n) = z ⨯ z ^ n
Beginning of Section CD_exp_nat_1_2
Hypothesis F_0 : F 0
Hypothesis F_1 : F 1
Hypothesis F_minus_0 : - 0 = 0
Hypothesis F_conj_0 : conj 0 = 0
Hypothesis F_conj_1 : conj 1 = 1
Hypothesis F_add_0L : ∀x, F x → 0 + x = x
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
End of Section CD_exp_nat_1_2
Hypothesis F_minus : ∀x, F x → F (- x)
Hypothesis F_conj : ∀x, F x → F (conj x)
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
Hypothesis F_0 : F 0
Hypothesis F_1 : F 1
End of Section CD_exp_nat
End of Section Alg