Beginning of Section Alg
(*** $I sig/Part1.mgs ***)
(*** $I sig/Part2.mgs ***)
(*** $I sig/Part3.mgs ***)
(*** $I sig/Part4.mgs ***)
(*** $I sig/Part5.mgs ***)
(*** $I sig/Part6.mgs ***)
(*** $I sig/Part7.mgs ***)
(*** $I sig/Part8.mgs ***)
(*** $I sig/Part9.mgs ***)
(*** $I sig/Part10.mgs ***)
(*** Part 11: Cayley Dickson ***)
L14
Variable extension_tag : set
L16
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha extension_tag
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.
L18
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...
L19
Variable F : set → prop
L21
Hypothesis extension_tag_fresh : ∀x, F x → ∀u ∈ x, extension_tag ∉ u
L23
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.
L34
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.
L52
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.
L59
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.
L81
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.
L91
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.
L115
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.
L125
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.
L133
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...
L135
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.
L145
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.
L159
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.
L170
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...
L172
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...
L173
Let proj0 ≝ CD_proj0
L175
Let proj1 ≝ CD_proj1
L176
Let pa : set → set → set ≝ pair_tag
L177
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.
L184
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.
L197
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.
L212
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.
L222
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.
L226
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.
L230
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.
L234
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.
L244
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.
L252
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
L262
Variable minus : set → set
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus.
L265
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.
L269
Variable conj : set → set
L272
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
L277
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.
L280
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
L286
Variable minus : set → set
L288
Variable conj : set → set
L289
Variable add : set → set → set
L290
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.
L295
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.
L298
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
L304
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.
L308
Hypothesis F_minus : ∀x, F x → F (- x)
L310
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.
L318
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.
L332
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.
L346
Variable conj : set → set
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.
L349
Hypothesis F_conj : ∀x, F x → F (conj x)
L351
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.
L359
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.
L373
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
L391
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.
L395
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L397
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.
L409
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.
L432
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
L459
Variable minus : set → set
L461
Variable conj : set → set
L462
Variable add : set → set → set
L463
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.
L473
Hypothesis F_minus : ∀x, F x → F (- x)
L475
Hypothesis F_conj : ∀x, F x → F (conj x)
L476
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L477
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L478
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.
L499
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.
L550
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
L605
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.
L609
Hypothesis F_0 : F 0
L611
Hypothesis F_minus_0 : - 0 = 0
L612
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.
L622
Variable conj : set → set
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term CD_conj minus conj.
L625
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
L639
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.
L644
Hypothesis F_0 : F 0
L646
Hypothesis F_add_0_0 : 0 + 0 = 0
L647
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
L663
Variable minus : set → set
L665
Variable conj : set → set
L666
Variable add : set → set → set
L667
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.
L677
Hypothesis F_0 : F 0
L679
Hypothesis F_conj : ∀x, F x → F (conj x)
L680
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L681
Hypothesis F_minus_0 : - 0 = 0
L682
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L683
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L684
Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L685
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
L707
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.
L711
Hypothesis F_minus : ∀x, F x → F (- x)
L713
Hypothesis F_minus_invol : ∀x, F x → - - x = x
L714
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
L738
Variable minus : set → set
L740
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.
L745
Hypothesis F_minus : ∀x, F x → F (- x)
L747
Hypothesis F_conj : ∀x, F x → F (conj x)
L748
Hypothesis F_minus_invol : ∀x, F x → - - x = x
L749
Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x
L750
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
L774
Variable minus : set → set
L776
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.
L781
Hypothesis F_minus : ∀x, F x → F (- x)
L783
Hypothesis F_conj : ∀x, F x → F (conj x)
L784
Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
L785
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
L821
Variable minus : set → set
L823
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.
L830
Hypothesis F_minus : ∀x, F x → F (- x)
L832
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L833
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L834
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
L885
Variable minus : set → set
L887
Variable conj : set → set
L888
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.
L896
Hypothesis F_minus : ∀x, F x → F (- x)
L898
Hypothesis F_conj : ∀x, F x → F (conj x)
L899
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L900
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L901
Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L902
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
L953
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.
L957
Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L959
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
L985
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.
L989
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L991
Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
L992
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
L1050
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.
L1054
Hypothesis F_0 : F 0
L1056
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L1057
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
L1077
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.
L1081
Hypothesis F_0 : F 0
L1083
Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L1084
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
L1104
Variable minus : set → set
L1106
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.
L1111
Hypothesis F_minus : ∀x, F x → F (- x)
L1113
Hypothesis F_add_minus_linv : ∀x, F x → - x + x = 0
L1114
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
L1140
Variable minus : set → set
L1142
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.
L1147
Hypothesis F_minus : ∀x, F x → F (- x)
L1149
Hypothesis F_add_minus_rinv : ∀x, F x → x + - x = 0
L1150
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
L1175
Variable minus : set → set
L1177
Variable conj : set → set
L1178
Variable add : set → set → set
L1179
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.
L1188
Hypothesis F_0 : F 0
L1190
Hypothesis F_minus_0 : - 0 = 0
L1191
Hypothesis F_conj_0 : conj 0 = 0
L1192
Hypothesis F_add_0_0 : 0 + 0 = 0
L1193
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L1194
Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L1195
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
L1228
Variable minus : set → set
L1230
Variable conj : set → set
L1231
Variable add : set → set → set
L1232
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.
L1241
Hypothesis F_0 : F 0
L1243
Hypothesis F_conj : ∀x, F x → F (conj x)
L1244
Hypothesis F_minus_0 : - 0 = 0
L1245
Hypothesis F_add_0_0 : 0 + 0 = 0
L1246
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L1247
Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L1248
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
L1281
Variable minus : set → set
L1283
Variable conj : set → set
L1284
Variable add : set → set → set
L1285
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.
L1294
Hypothesis F_0 : F 0
L1296
Hypothesis F_1 : F 1
L1297
Hypothesis F_minus_0 : - 0 = 0
L1298
Hypothesis F_conj_0 : conj 0 = 0
L1299
Hypothesis F_conj_1 : conj 1 = 1
L1300
Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L1301
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L1302
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L1303
Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
L1304
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
L1344
Variable minus : set → set
L1346
Variable conj : set → set
L1347
Variable add : set → set → set
L1348
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.
L1357
Hypothesis F_0 : F 0
L1359
Hypothesis F_1 : F 1
L1360
Hypothesis F_conj : ∀x, F x → F (conj x)
L1361
Hypothesis F_minus_0 : - 0 = 0
L1362
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L1363
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L1364
Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L1365
Hypothesis F_mul_1L : ∀x, F x → 1 * x = x
L1366
Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
L1367
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
L1402
Variable minus : set → set
L1404
Variable conj : set → set
L1405
Variable add : set → set → set
L1406
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.
L1415
Hypothesis F_minus : ∀x, F x → F (- x)
L1417
Hypothesis F_conj : ∀x, F x → F (conj x)
L1418
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L1419
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L1420
Hypothesis F_minus_invol : ∀x, F x → - - x = x
L1421
Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x
L1422
Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
L1423
Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L1424
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L1425
Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L1426
Hypothesis F_conj_mul : ∀x y, F x → F y → conj (x * y) = conj y * conj x
L1427
Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L1428
Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
L1429
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
L1603
Variable minus : set → set
L1605
Variable conj : set → set
L1606
Variable add : set → set → set
L1607
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.
L1616
Hypothesis F_minus : ∀x, F x → F (- x)
L1618
Hypothesis F_conj : ∀x, F x → F (conj x)
L1619
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L1620
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L1621
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L1622
Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
L1623
Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L1624
Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z
L1625
Hypothesis F_add_mul_distrR : ∀x y z, F x → F y → F z → (x + y) * z = x * z + y * z
L1626
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
L1789
Variable minus : set → set
L1791
Variable conj : set → set
L1792
Variable add : set → set → set
L1793
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.
L1802
Hypothesis F_minus : ∀x, F x → F (- x)
L1804
Hypothesis F_conj : ∀x, F x → F (conj x)
L1805
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L1806
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L1807
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L1808
Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L1809
Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
L1810
Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L1811
Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z
L1812
Hypothesis F_add_mul_distrR : ∀x y z, F x → F y → F z → (x + y) * z = x * z + y * z
L1813
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
L1972
Variable minus : set → set
L1974
Variable conj : set → set
L1975
Variable add : set → set → set
L1976
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.
L1985
Hypothesis F_minus : ∀x, F x → F (- x)
L1987
Hypothesis F_conj : ∀x, F x → F (conj x)
L1988
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L1989
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L1990
Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
L1991
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L1992
Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L1993
Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
L1994
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
L2088
Variable minus : set → set
L2090
Variable conj : set → set
L2091
Variable add : set → set → set
L2092
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.
L2101
Hypothesis F_minus : ∀x, F x → F (- x)
L2103
Hypothesis F_conj : ∀x, F x → F (conj x)
L2104
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L2105
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L2106
Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L2107
Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L2108
Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
L2109
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
L2200
Variable minus : set → set
L2202
Variable conj : set → set
L2203
Variable add : set → set → set
L2204
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.
L2216
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.
L2221
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
L2228
Hypothesis F_0 : F 0
L2230
Hypothesis F_1 : F 1
L2231
Hypothesis F_minus_0 : - 0 = 0
L2232
Hypothesis F_conj_0 : conj 0 = 0
L2233
Hypothesis F_conj_1 : conj 1 = 1
L2234
Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L2235
Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L2236
Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L2237
Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
L2238
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.
L2247
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
L2257
Hypothesis F_minus : ∀x, F x → F (- x)
L2259
Hypothesis F_conj : ∀x, F x → F (conj x)
L2260
Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L2261
Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L2262
Hypothesis F_0 : F 0
L2264
Hypothesis F_1 : F 1
L2265
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