Beginning of Section Alg
L12Variable extension_tag : set
L13Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha extension_tag
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
L16Definition. We define
pair_tag to be
λx y ⇒ x ∪ {u ''|u ∈ y} of type
set → set → set.
L17Variable F : set → prop
L18Hypothesis extension_tag_fresh : ∀x, F x → ∀u ∈ x, extension_tag ∉ u
L21Axiom. (
ctagged_eqE_eq) We take the following as an axiom:
∀x y, F x → F y → ∀u ∈ x, ∀v ∈ y, u '' = v '' → u = v
L26Axiom. (
pair_tag_0) We take the following as an axiom:
Primitive. The name
CD_carr is a term of type
set → prop.
L29Axiom. (
CD_carr_I) We take the following as an axiom:
L30Axiom. (
CD_carr_E) We take the following as an axiom:
L32Definition. We define
CD_proj0 to be
λz ⇒ Eps_i (λx ⇒ F x ∧ ∃y, F y ∧ z = pair_tag x y) of type
set → set.
L37Axiom. (
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
L38Axiom. (
CD_proj0_2) We take the following as an axiom:
∀x y, F x → F y → proj0 (pa x y) = x
L39Axiom. (
CD_proj1_1) We take the following as an axiom:
∀z, CD_carr z → F (proj1 z) ∧ z = pa (proj0 z) (proj1 z)
L40Axiom. (
CD_proj1_2) We take the following as an axiom:
∀x y, F x → F y → proj1 (pa x y) = y
L41Axiom. (
CD_proj0R) We take the following as an axiom:
L42Axiom. (
CD_proj1R) We take the following as an axiom:
L45Axiom. (
CD_proj0_F) We take the following as an axiom:
L46Axiom. (
CD_proj1_F) We take the following as an axiom:
Beginning of Section CD_minus_conj
L48Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
L50Definition. 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.
L52Variable conj : set → set
L53Definition. 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
L56Variable 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.
L58Definition. 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
L61Variable minus : set → set
L62Variable conj : set → set
L63Variable add : set → set → set
L64Variable 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.
L68Definition. 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.
L70Definition. 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
L73Variable 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.
L76Hypothesis F_minus : ∀x, F x → F (- x)
L77Axiom. (
CD_minus_CD) We take the following as an axiom:
L80Variable conj : set → set
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
L82Hypothesis F_conj : ∀x, F x → F (conj x)
L83Axiom. (
CD_conj_CD) We take the following as an axiom:
End of Section CD_minus_conj_clos
Beginning of Section CD_add_clos
L88Variable 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.
L91Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L92Axiom. (
CD_add_CD) We take the following as an axiom:
End of Section CD_add_clos
Beginning of Section CD_mul_clos
L97Variable minus : set → set
L98Variable conj : set → set
L99Variable add : set → set → set
L100Variable 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.
L108Hypothesis F_minus : ∀x, F x → F (- x)
L109Hypothesis F_conj : ∀x, F x → F (conj x)
L110Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L111Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L112Axiom. (
CD_mul_CD) We take the following as an axiom:
End of Section CD_mul_clos
Beginning of Section CD_minus_conj_F
L117Variable 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.
L121Hypothesis F_minus_0 : - 0 = 0
L123Variable 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
L128Variable 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.
L132Hypothesis F_add_0_0 : 0 + 0 = 0
L133Axiom. (
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
L136Variable minus : set → set
L137Variable conj : set → set
L138Variable add : set → set → set
L139Variable 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.
L148Hypothesis F_conj : ∀x, F x → F (conj x)
L149Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L150Hypothesis F_minus_0 : - 0 = 0
L151Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L152Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L153Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L154Axiom. (
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
L157Variable 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.
L160Hypothesis F_minus : ∀x, F x → F (- x)
L161Hypothesis F_minus_invol : ∀x, F x → - - x = x
End of Section CD_minus_invol
Beginning of Section CD_conj_invol
L165Variable minus : set → set
L166Variable 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.
L170Hypothesis F_minus : ∀x, F x → F (- x)
L171Hypothesis F_conj : ∀x, F x → F (conj x)
L172Hypothesis F_minus_invol : ∀x, F x → - - x = x
L173Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x
End of Section CD_conj_invol
Beginning of Section CD_conj_minus
L177Variable minus : set → set
L178Variable 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.
L182Hypothesis F_minus : ∀x, F x → F (- x)
L183Hypothesis F_conj : ∀x, F x → F (conj x)
L184Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
End of Section CD_conj_minus
Beginning of Section CD_minus_add
L188Variable minus : set → set
L189Variable 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.
L194Hypothesis F_minus : ∀x, F x → F (- x)
L195Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L196Hypothesis 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
L200Variable minus : set → set
L201Variable conj : set → set
L202Variable 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.
L208Hypothesis F_minus : ∀x, F x → F (- x)
L209Hypothesis F_conj : ∀x, F x → F (conj x)
L210Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L211Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L212Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L213Axiom. (
CD_conj_add) We take the following as an axiom:
End of Section CD_conj_add
Beginning of Section CD_add_com
L216Variable 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.
L219Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L220Axiom. (
CD_add_com) We take the following as an axiom:
End of Section CD_add_com
Beginning of Section CD_add_assoc
L223Variable 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.
L226Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L227Hypothesis 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
L231Variable 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.
L235Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L236Axiom. (
CD_add_0R) We take the following as an axiom:
End of Section CD_add_0R
Beginning of Section CD_add_0L
L239Variable 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.
L243Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L244Axiom. (
CD_add_0L) We take the following as an axiom:
End of Section CD_add_0L
Beginning of Section CD_add_minus_linv
L247Variable minus : set → set
L248Variable 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.
L253Hypothesis F_minus : ∀x, F x → F (- x)
L254Hypothesis F_add_minus_linv : ∀x, F x → - x + x = 0
End of Section CD_add_minus_linv
Beginning of Section CD_add_minus_rinv
L258Variable minus : set → set
L259Variable 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.
L264Hypothesis F_minus : ∀x, F x → F (- x)
L265Hypothesis F_add_minus_rinv : ∀x, F x → x + - x = 0
End of Section CD_add_minus_rinv
Beginning of Section CD_mul_0R
L269Variable minus : set → set
L270Variable conj : set → set
L271Variable add : set → set → set
L272Variable 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.
L281Hypothesis F_minus_0 : - 0 = 0
L282Hypothesis F_conj_0 : conj 0 = 0
L283Hypothesis F_add_0_0 : 0 + 0 = 0
L284Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L285Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L286Axiom. (
CD_mul_0R) We take the following as an axiom:
End of Section CD_mul_0R
Beginning of Section CD_mul_0L
L289Variable minus : set → set
L290Variable conj : set → set
L291Variable add : set → set → set
L292Variable 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.
L301Hypothesis F_conj : ∀x, F x → F (conj x)
L302Hypothesis F_minus_0 : - 0 = 0
L303Hypothesis F_add_0_0 : 0 + 0 = 0
L304Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L305Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L306Axiom. (
CD_mul_0L) We take the following as an axiom:
End of Section CD_mul_0L
Beginning of Section CD_mul_1R
L309Variable minus : set → set
L310Variable conj : set → set
L311Variable add : set → set → set
L312Variable 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.
L322Hypothesis F_minus_0 : - 0 = 0
L323Hypothesis F_conj_0 : conj 0 = 0
L324Hypothesis F_conj_1 : conj 1 = 1
L325Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L326Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L327Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L328Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
L329Axiom. (
CD_mul_1R) We take the following as an axiom:
End of Section CD_mul_1R
Beginning of Section CD_mul_1L
L332Variable minus : set → set
L333Variable conj : set → set
L334Variable add : set → set → set
L335Variable 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.
L345Hypothesis F_conj : ∀x, F x → F (conj x)
L346Hypothesis F_minus_0 : - 0 = 0
L347Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L348Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L349Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L350Hypothesis F_mul_1L : ∀x, F x → 1 * x = x
L351Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
L352Axiom. (
CD_mul_1L) We take the following as an axiom:
End of Section CD_mul_1L
Beginning of Section CD_conj_mul
L355Variable minus : set → set
L356Variable conj : set → set
L357Variable add : set → set → set
L358Variable 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.
L366Hypothesis F_minus : ∀x, F x → F (- x)
L367Hypothesis F_conj : ∀x, F x → F (conj x)
L368Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L369Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L370Hypothesis F_minus_invol : ∀x, F x → - - x = x
L371Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x
L372Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
L373Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L374Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L375Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L376Hypothesis F_conj_mul : ∀x y, F x → F y → conj (x * y) = conj y * conj x
L377Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L378Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
L379Axiom. (
CD_conj_mul) We take the following as an axiom:
End of Section CD_conj_mul
Beginning of Section CD_add_mul_distrR
L382Variable minus : set → set
L383Variable conj : set → set
L384Variable add : set → set → set
L385Variable 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.
L393Hypothesis F_minus : ∀x, F x → F (- x)
L394Hypothesis F_conj : ∀x, F x → F (conj x)
L395Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L396Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L397Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L398Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
L399Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L400Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z
L401Hypothesis 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
L405Variable minus : set → set
L406Variable conj : set → set
L407Variable add : set → set → set
L408Variable 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.
L416Hypothesis F_minus : ∀x, F x → F (- x)
L417Hypothesis F_conj : ∀x, F x → F (conj x)
L418Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L419Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L420Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L421Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L422Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
L423Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L424Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z
L425Hypothesis 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
L429Variable minus : set → set
L430Variable conj : set → set
L431Variable add : set → set → set
L432Variable 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.
L440Hypothesis F_minus : ∀x, F x → F (- x)
L441Hypothesis F_conj : ∀x, F x → F (conj x)
L442Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L443Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L444Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
L445Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L446Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L447Hypothesis 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
L451Variable minus : set → set
L452Variable conj : set → set
L453Variable add : set → set → set
L454Variable 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.
L462Hypothesis F_minus : ∀x, F x → F (- x)
L463Hypothesis F_conj : ∀x, F x → F (conj x)
L464Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L465Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L466Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L467Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L468Hypothesis 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
L472Variable minus : set → set
L473Variable conj : set → set
L474Variable add : set → set → set
L475Variable 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.
L486Axiom. (
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
L490Hypothesis F_minus_0 : - 0 = 0
L491Hypothesis F_conj_0 : conj 0 = 0
L492Hypothesis F_conj_1 : conj 1 = 1
L493Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L494Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L495Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L496Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
End of Section CD_exp_nat_1_2
L500Hypothesis F_minus : ∀x, F x → F (- x)
L501Hypothesis F_conj : ∀x, F x → F (conj x)
L502Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L503Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
End of Section CD_exp_nat
End of Section Alg