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.
In Proofgold the corresponding term root is abc4d9... and object id is 76732f...
Variable F : set → prop
Hypothesis extension_tag_fresh : ∀x, F x → ∀u ∈ x, extension_tag ∉ u
Theorem. (ctagged_notin_F)
∀x y, F x → (y '') ∉ x
In Proofgold the corresponding term root is 67cee9... and proposition id is 8b7e9e...
Proof:
Proof not loaded.
Theorem. (ctagged_eqE_Subq)
∀x y, F x → ∀u ∈ x, ∀v, u '' = v '' → u ⊆ v
In Proofgold the corresponding term root is a506f8... and proposition id is cbce18...
Proof:
Proof not loaded.
Theorem. (ctagged_eqE_eq)
∀x y, F x → F y → ∀u ∈ x, ∀v ∈ y, u '' = v '' → u = v
In Proofgold the corresponding term root is 80ff51... and proposition id is 397f7d...
Proof:
Proof not loaded.
Theorem. (pair_tag_prop_1_Subq)
∀x1 y1 x2 y2, F x1 → pair_tag x1 y1 = pair_tag x2 y2 → x1 ⊆ x2
In Proofgold the corresponding term root is 7d9199... and proposition id is a3ef42...
Proof:
Proof not loaded.
Theorem. (pair_tag_prop_1)
∀x1 y1 x2 y2, F x1 → F x2 → pair_tag x1 y1 = pair_tag x2 y2 → x1 = x2
In Proofgold the corresponding term root is 6d65de... and proposition id is a92ff7...
Proof:
Proof not loaded.
Theorem. (pair_tag_prop_2_Subq)
∀x1 y1 x2 y2, F y1 → F x2 → F y2 → pair_tag x1 y1 = pair_tag x2 y2 → y1 ⊆ y2
In Proofgold the corresponding term root is 51b765... and proposition id is f24efc...
Proof:
Proof not loaded.
Theorem. (pair_tag_prop_2)
∀x1 y1 x2 y2, F x1 → F y1 → F x2 → F y2 → pair_tag x1 y1 = pair_tag x2 y2 → y1 = y2
In Proofgold the corresponding term root is 5f9628... and proposition id is e5fc85...
Proof:
Proof not loaded.
Theorem. (pair_tag_0)
∀x, pair_tag x 0 = x
In Proofgold the corresponding term root is 67646d... and proposition id is 38d429...
Proof:
Proof not loaded.
Definition. We define CD_carr to be λz ⇒ ∃x, F x ∧ ∃y, F y ∧ z = pair_tag x y of type set → prop.
In Proofgold the corresponding term root is 0c2c09... and object id is 787a60...
Theorem. (CD_carr_I)
∀x y, F x → F y → CD_carr (pair_tag x y)
In Proofgold the corresponding term root is 7da562... and proposition id is ff1d14...
Proof:
Proof not loaded.
Theorem. (CD_carr_E)
∀z, CD_carr z → ∀p : set → prop, (∀x y, F x → F y → z = pair_tag x y → p (pair_tag x y)) → p z
In Proofgold the corresponding term root is 6d3181... and proposition id is 72fbc5...
Proof:
Proof not loaded.
Theorem. (CD_carr_0ext)
F 0 → ∀x, F x → CD_carr x
In Proofgold the corresponding term root is 0fb20d... and proposition id is ed952a...
Proof:
Proof not loaded.
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.
In Proofgold the corresponding term root is e6d3c9... and object id is 672bda...
Definition. We define CD_proj1 to be λz ⇒ Eps_i (λy ⇒ F y ∧ z = pair_tag (CD_proj0 z) y) of type set → set.
In Proofgold the corresponding term root is 934eed... and object id is e1c3ce...
Let proj0 ≝ CD_proj0
Let proj1 ≝ CD_proj1
Let pa : set → set → set ≝ pair_tag
Theorem. (CD_proj0_1)
∀z, CD_carr z → F (proj0 z) ∧ ∃y, F y ∧ z = pa (proj0 z) y
In Proofgold the corresponding term root is cd8c23... and proposition id is e9b94d...
Proof:
Proof not loaded.
Theorem. (CD_proj0_2)
∀x y, F x → F y → proj0 (pa x y) = x
In Proofgold the corresponding term root is 58ae60... and proposition id is d0a094...
Proof:
Proof not loaded.
Theorem. (CD_proj1_1)
∀z, CD_carr z → F (proj1 z) ∧ z = pa (proj0 z) (proj1 z)
In Proofgold the corresponding term root is 29b7ad... and proposition id is da2481...
Proof:
Proof not loaded.
Theorem. (CD_proj1_2)
∀x y, F x → F y → proj1 (pa x y) = y
In Proofgold the corresponding term root is 582e7f... and proposition id is 006468...
Proof:
Proof not loaded.
Theorem. (CD_proj0R)
∀z, CD_carr z → F (proj0 z)
In Proofgold the corresponding term root is db089e... and proposition id is 0344a9...
Proof:
Proof not loaded.
Theorem. (CD_proj1R)
∀z, CD_carr z → F (proj1 z)
In Proofgold the corresponding term root is 79b5f6... and proposition id is 197fac...
Proof:
Proof not loaded.
Theorem. (CD_proj0proj1_eta)
∀z, CD_carr z → z = pa (proj0 z) (proj1 z)
In Proofgold the corresponding term root is 005546... and proposition id is 9f625c...
Proof:
Proof not loaded.
Theorem. (CD_proj0proj1_split)
∀z w, CD_carr z → CD_carr w → proj0 z = proj0 w → proj1 z = proj1 w → z = w
In Proofgold the corresponding term root is de0617... and proposition id is 6f6778...
Proof:
Proof not loaded.
Theorem. (CD_proj0_F)
F 0 → ∀x, F x → CD_proj0 x = x
In Proofgold the corresponding term root is b4c9a8... and proposition id is 0324b7...
Proof:
Proof not loaded.
Theorem. (CD_proj1_F)
F 0 → ∀x, F x → CD_proj1 x = 0
In Proofgold the corresponding term root is 40d7ac... and proposition id is 0861dd...
Proof:
Proof not loaded.
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.
In Proofgold the corresponding term root is 2d3588... and object id is 87e4d7...
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.
In Proofgold the corresponding term root is b39bd2... and object id is 05d4c2...
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.
In Proofgold the corresponding term root is 7a5ff6... and object id is ac7808...
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.
In Proofgold the corresponding term root is f53b0e... and object id is a0aea9...
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.
In Proofgold the corresponding term root is 7fdc79... and object id is 750c11...
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)
Theorem. (CD_minus_CD)
∀z, CD_carr z → CD_carr (:-: z)
In Proofgold the corresponding term root is 04b152... and proposition id is e2afae...
Proof:
Proof not loaded.
Theorem. (CD_minus_proj0)
∀z, CD_carr z → proj0 (:-: z) = - proj0 z
In Proofgold the corresponding term root is 746fe1... and proposition id is ad320c...
Proof:
Proof not loaded.
Theorem. (CD_minus_proj1)
∀z, CD_carr z → proj1 (:-: z) = - proj1 z
In Proofgold the corresponding term root is 93a203... and proposition id is 4e5c97...
Proof:
Proof not loaded.
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)
Theorem. (CD_conj_CD)
∀z, CD_carr z → CD_carr (z ')
In Proofgold the corresponding term root is 78d930... and proposition id is 541129...
Proof:
Proof not loaded.
Theorem. (CD_conj_proj0)
∀z, CD_carr z → proj0 (z ') = conj (proj0 z)
In Proofgold the corresponding term root is a61a2e... and proposition id is 2104b7...
Proof:
Proof not loaded.
Theorem. (CD_conj_proj1)
∀z, CD_carr z → proj1 (z ') = - proj1 z
In Proofgold the corresponding term root is c56033... and proposition id is 2bf262...
Proof:
Proof not loaded.
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)
Theorem. (CD_add_CD)
∀z w, CD_carr z → CD_carr w → CD_carr (z + w)
In Proofgold the corresponding term root is 7c6f64... and proposition id is ff60d4...
Proof:
Proof not loaded.
Theorem. (CD_add_proj0)
∀z w, CD_carr z → CD_carr w → proj0 (z + w) = proj0 z + proj0 w
In Proofgold the corresponding term root is 76fd56... and proposition id is 258b8b...
Proof:
Proof not loaded.
Theorem. (CD_add_proj1)
∀z w, CD_carr z → CD_carr w → proj1 (z + w) = proj1 z + proj1 w
In Proofgold the corresponding term root is 1454b7... and proposition id is 2b4a1d...
Proof:
Proof not loaded.
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)
Theorem. (CD_mul_CD)
∀z w, CD_carr z → CD_carr w → CD_carr (z ⨯ w)
In Proofgold the corresponding term root is bda919... and proposition id is 6fa963...
Proof:
Proof not loaded.
Theorem. (CD_mul_proj0)
∀z w, CD_carr z → CD_carr w → proj0 (z ⨯ w) = proj0 z * proj0 w + - conj (proj1 w) * proj1 z
In Proofgold the corresponding term root is 7b8951... and proposition id is 411462...
Proof:
Proof not loaded.
Theorem. (CD_mul_proj1)
∀z w, CD_carr z → CD_carr w → proj1 (z ⨯ w) = proj1 w * proj0 z + proj1 z * conj (proj0 w)
In Proofgold the corresponding term root is 053f09... and proposition id is 752898...
Proof:
Proof not loaded.
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
Theorem. (CD_minus_F_eq)
∀x, F x → :-: x = - x
In Proofgold the corresponding term root is 73ac62... and proposition id is 411826...
Proof:
Proof not loaded.
Variable conj : set → set
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.
Theorem. (CD_conj_F_eq)
∀x, F x → x ' = conj x
In Proofgold the corresponding term root is a2640a... and proposition id is e715f1...
Proof:
Proof not loaded.
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
Theorem. (CD_add_F_eq)
∀x y, F x → F y → x + y = x + y
In Proofgold the corresponding term root is 2e70a4... and proposition id is a784d9...
Proof:
Proof not loaded.
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
Theorem. (CD_mul_F_eq)
∀x y, F x → F y → x ⨯ y = x * y
In Proofgold the corresponding term root is 3f44c9... and proposition id is 53183f...
Proof:
Proof not loaded.
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
Theorem. (CD_minus_invol)
∀z, CD_carr z → :-: :-: z = z
In Proofgold the corresponding term root is 8564c2... and proposition id is 69beaf...
Proof:
Proof not loaded.
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
Theorem. (CD_conj_invol)
∀z, CD_carr z → z ' ' = z
In Proofgold the corresponding term root is f325ba... and proposition id is b1a97e...
Proof:
Proof not loaded.
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
Theorem. (CD_conj_minus)
∀z, CD_carr z → (:-: z) ' = :-: (z ')
In Proofgold the corresponding term root is 2e6a97... and proposition id is f23f1d...
Proof:
Proof not loaded.
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
Theorem. (CD_minus_add)
∀z w, CD_carr z → CD_carr w → :-: (z + w) = :-: z + :-: w
In Proofgold the corresponding term root is 1b8b02... and proposition id is fb82f8...
Proof:
Proof not loaded.
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
Theorem. (CD_conj_add)
∀z w, CD_carr z → CD_carr w → (z + w) ' = z ' + w '
In Proofgold the corresponding term root is ac016f... and proposition id is 643b33...
Proof:
Proof not loaded.
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
Theorem. (CD_add_com)
∀z w, CD_carr z → CD_carr w → z + w = w + z
In Proofgold the corresponding term root is bf081b... and proposition id is 5fc91f...
Proof:
Proof not loaded.
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)
Theorem. (CD_add_assoc)
∀z w u, CD_carr z → CD_carr w → CD_carr u → (z + w) + u = z + (w + u)
In Proofgold the corresponding term root is ba31a4... and proposition id is c59c2a...
Proof:
Proof not loaded.
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
Theorem. (CD_add_0R)
∀z, CD_carr z → z + 0 = z
In Proofgold the corresponding term root is 553cb8... and proposition id is 53e78d...
Proof:
Proof not loaded.
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
Theorem. (CD_add_0L)
∀z, CD_carr z → 0 + z = z
In Proofgold the corresponding term root is d80ef4... and proposition id is 662b89...
Proof:
Proof not loaded.
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
Theorem. (CD_add_minus_linv)
∀z, CD_carr z → :-: z + z = 0
In Proofgold the corresponding term root is 65a657... and proposition id is 477b97...
Proof:
Proof not loaded.
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
Theorem. (CD_add_minus_rinv)
∀z, CD_carr z → z + :-: z = 0
In Proofgold the corresponding term root is 6dffee... and proposition id is 7008fd...
Proof:
Proof not loaded.
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
Theorem. (CD_mul_0R)
∀z, CD_carr z → z ⨯ 0 = 0
In Proofgold the corresponding term root is 9cc913... and proposition id is a15017...
Proof:
Proof not loaded.
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
Theorem. (CD_mul_0L)
∀z, CD_carr z → 0 ⨯ z = 0
In Proofgold the corresponding term root is ab8edf... and proposition id is 31e944...
Proof:
Proof not loaded.
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
Theorem. (CD_mul_1R)
∀z, CD_carr z → z ⨯ 1 = z
In Proofgold the corresponding term root is c55555... and proposition id is 62bb45...
Proof:
Proof not loaded.
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
Theorem. (CD_mul_1L)
∀z, CD_carr z → 1 ⨯ z = z
In Proofgold the corresponding term root is f83f52... and proposition id is 15a3f1...
Proof:
Proof not loaded.
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)
Theorem. (CD_conj_mul)
∀z w, CD_carr z → CD_carr w → (z ⨯ w) ' = w ' ⨯ z '
In Proofgold the corresponding term root is b927f8... and proposition id is 19c917...
Proof:
Proof not loaded.
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
Theorem. (CD_add_mul_distrR)
∀z w u, CD_carr z → CD_carr w → CD_carr u → (z + w) ⨯ u = z ⨯ u + w ⨯ u
In Proofgold the corresponding term root is 3ea8d0... and proposition id is dfcffc...
Proof:
Proof not loaded.
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
Theorem. (CD_add_mul_distrL)
∀z w u, CD_carr z → CD_carr w → CD_carr u → z ⨯ (w + u) = z ⨯ w + z ⨯ u
In Proofgold the corresponding term root is 45d05f... and proposition id is 447dab...
Proof:
Proof not loaded.
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)
Theorem. (CD_minus_mul_distrR)
∀z w, CD_carr z → CD_carr w → z ⨯ (:-: w) = :-: z ⨯ w
In Proofgold the corresponding term root is 92051e... and proposition id is 34f645...
Proof:
Proof not loaded.
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)
Theorem. (CD_minus_mul_distrL)
∀z w, CD_carr z → CD_carr w → (:-: z) ⨯ w = :-: z ⨯ w
In Proofgold the corresponding term root is 8f6dad... and proposition id is bd692d...
Proof:
Proof not loaded.
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.
Theorem. (CD_exp_nat_0)
∀z, z ^ 0 = 1
In Proofgold the corresponding term root is f63bba... and proposition id is 2c1506...
Proof:
Proof not loaded.
Theorem. (CD_exp_nat_S)
∀z n, nat_p n → z ^ (ordsucc n) = z ⨯ z ^ n
In Proofgold the corresponding term root is 56eeed... and proposition id is 5b5f54...
Proof:
Proof not loaded.
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
Theorem. (CD_exp_nat_1)
∀z, CD_carr z → z ^ 1 = z
In Proofgold the corresponding term root is cbb149... and proposition id is e01fe9...
Proof:
Proof not loaded.
Theorem. (CD_exp_nat_2)
∀z, CD_carr z → z ^ 2 = z ⨯ z
In Proofgold the corresponding term root is c5241d... and proposition id is 9b74d2...
Proof:
Proof not loaded.
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
Theorem. (CD_exp_nat_CD)
∀z, CD_carr z → ∀n, nat_p n → CD_carr (z ^ n)
In Proofgold the corresponding term root is 43212b... and proposition id is a1e10b...
Proof:
Proof not loaded.
End of Section CD_exp_nat
End of Section Alg