Merge branch 'levitation'

Interface talk/B/a/s/Basic arithmetic

@@ -15,4 +15,4 @@ Maybes:
 
 * a ≠ 0 ↔ a > 0 (easy consequence of ZeroSmallest and LessThanLessEqual)
 
-[[User:Kingdon|Kingdon]] 14:13, 8 September 2010 (UTC)
+[[User:Kingdon|Kingdon]] 14:13, 8 September 2010 (UTC)

Interface/B/a/s/Basic arithmetic

@@ -230,4 +230,4 @@ stmt (Induction6 ((n a) (φ0 n) (φk n) (φSk n) (φa n) (φ k) (n k))
   φa)
 </jh>
 
-[[Category:Elementary number theory|{{PAGENAME}}]]
+[[Category:Elementary number theory|{{PAGENAME}}]]

Main/B/a/s/Basic arithmetic

@@ -1894,19 +1894,31 @@ thm (LessEqualLessThan () () ((a ≤ b) ↔ ((a < b) ∨ (a = b))) (
         swapBiconditional
         applyBiconditionalTransitivity
 </jh>
+<<<<<<< HEAD
 That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>.  But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code>&lt;</code>, so this is enough.
+=======
+That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>.  But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code><</code>, so this is enough.
+>>>>>>> 4ca49c20ca2749b97b475fb73c350452237d11cd
 <jh>
 ))
 </jh>
 
+<<<<<<< HEAD
 For parallelism, we also provide the definition of <code>&lt;</code> as a theorem.
+=======
+For parallelism, we also provide the definition of <code><</code> as a theorem.
+>>>>>>> 4ca49c20ca2749b97b475fb73c350452237d11cd
 <jh>
 thm (LessThanLessEqual () () ((a < b) ↔ ((a ≤ b) ∧ (a ≠ b))) (
         (a < b) BiconditionalReflexivity
 ))
 </jh>
 
+<<<<<<< HEAD
 The builder for <code>&lt;</code> is a consequence of the one for <code>≤</code>.
+=======
+The builder for <code><</code> is a consequence of the one for <code>≤</code>.
+>>>>>>> 4ca49c20ca2749b97b475fb73c350452237d11cd
 
 <jh>
 thm (LessThanBuilder () () (((a0 = a1) ∧ (b0 = b1)) → ((a0 < b0) ↔ (a1 < b1))) (
@@ -1952,7 +1964,11 @@ thm (buildLessThanRR () ((HA (a0 = a1))) ((a0 < b) ↔ (a1 < b)) (
 </jh>
 
 ==== Transitivity ====
+<<<<<<< HEAD
 We start by proving that <code>a ≤ b ∧ b < c → a < c</code>. This has transitivity for <code>&lt;</code> as an immediate consequence, but will occasionally be useful in its own right.
+=======
+We start by proving that <code>a ≤ b ∧ b < c → a < c</code>. This has transitivity for <code><</code> as an immediate consequence, but will occasionally be useful in its own right.
+>>>>>>> 4ca49c20ca2749b97b475fb73c350452237d11cd
 
 The first lemma constitutes the easy part of the proof.
 <jh>
@@ -2016,7 +2032,11 @@ And a transposition finishes the job.
 ))
 </jh>
 
+<<<<<<< HEAD
 Combining the two lemmas gives us transitivity for <code>a ≤ b ∧ b &lt; c</code>.
+=======
+Combining the two lemmas gives us transitivity for <code>a ≤ b ∧ b < c</code>.
+>>>>>>> 4ca49c20ca2749b97b475fb73c350452237d11cd
 <jh>
 thm (LessEqualLessThanTransitivity () () (((a ≤ b) ∧ (b < c)) → (a < c)) (
         a b c  LessEqualLessThanTransitivity-1
@@ -2025,7 +2045,11 @@ thm (LessEqualLessThanTransitivity () () (((a ≤ b) ∧ (b < c)) → (a < c)) (
 ))
 </jh>
 
+<<<<<<< HEAD
 Transitivity for <code>&lt;</code> is an immediate consequence.
+=======
+Transitivity for <code><</code> is an immediate consequence.
+>>>>>>> 4ca49c20ca2749b97b475fb73c350452237d11cd
 <jh>
 thm (LessThanLessEqualImplication () () ((a < b) → (a ≤ b)) (
         (a ≤ b) (a ≠ b) ConjunctionRightElimination
@@ -2042,7 +2066,11 @@ thm (LessThanTransitivity () () (((a < b) ∧ (b < c)) → (a < c)) (
 </jh>
 
 ==== Strict order totality ====
+<<<<<<< HEAD
 Exactly one of <code>a &lt; b</code>, <code>a = b</code>, or <code>a &gt; b</code> holds. We start with the proposition that at least one of the three holds.
+=======
+Exactly one of <code>a < b</code>, <code>a = b</code>, or <code>a > b</code> holds. We start with the proposition that at least one of the three holds.
+>>>>>>> 4ca49c20ca2749b97b475fb73c350452237d11cd
 <jh>
 thm (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)) (
 </jh>
@@ -2074,7 +2102,11 @@ We just need to do some rearranging to finish.
 ))
 </jh>
 
+<<<<<<< HEAD
 The following theorems imply that no more than one of <code>a &lt; b</code>, <code>a = b</code>, or <code>a &gt; b</code> holds.
+=======
+The following theorems imply that no more than one of <code>a < b</code>, <code>a = b</code>, or <code>a > b</code> holds.
+>>>>>>> 4ca49c20ca2749b97b475fb73c350452237d11cd
 <jh>
 thm (LessThanEquality () () ((a < b) → (a ≠ b)) (
         a b LessThanLessEqual
@@ -2361,4 +2393,4 @@ export (ARITHMETIC Interface:Basic_arithmetic (CLASSICAL FIRSTORDER) ())
 == References ==
 <references/>
 
-[[Category:Elementary number theory|{{PAGENAME}}]]
+[[Category:Elementary number theory|{{PAGENAME}}]]

Talk/P/r/i/Principia Mathematica propositional logic

@@ -63,4 +63,4 @@ Need this link also go to the main page?
 
 [[User:Janburse|Janburse]] 13:19, 10 March 2012 (UTC)
 
-:I suppose I have no objection if you want to add it as an external link. It is a bit different in emphasis than this page (pmproofs is about finding shortest possible proofs, directly from axioms, whereas here we look for proofs which are clear and/or which closely follow the proofs given in ''Principia'', with no reluctance to use previously proved theorems). [[User:Kingdon|Kingdon]] 19:02, 10 March 2012 (UTC)
+:I suppose I have no objection if you want to add it as an external link. It is a bit different in emphasis than this page (pmproofs is about finding shortest possible proofs, directly from axioms, whereas here we look for proofs which are clear and/or which closely follow the proofs given in ''Principia'', with no reluctance to use previously proved theorems). [[User:Kingdon|Kingdon]] 19:02, 10 March 2012 (UTC)

User module/J/u/l/Julian sandbox

@@ -117,4 +117,4 @@ thm (2+2=4 () () (((2) + (2)) = (4)) (
 
 ))
 
-</jh>
+</jh>

User talk/R/a/p/Raph

@@ -37,4 +37,4 @@ If I go to the subversion version 9 of peano_thms.gh, I see the following (extra
     A y ([/] y x ph) sbc5
       y x ph sbc5
 
-Shoudn't the second invocation of sbc5 blow up because there isn't a distinct variable constraint on (x y)? If not, why not? Is this a bug in the var/tvar code? I don't see a reason why being a var rather than a tvar could soundly bypass distinct variable constraints, but I could have missed something. [[User:Kingdon|Kingdon]] 20:08, 12 June 2010 (UTC)
+Shoudn't the second invocation of sbc5 blow up because there isn't a distinct variable constraint on (x y)? If not, why not? Is this a bug in the var/tvar code? I don't see a reason why being a var rather than a tvar could soundly bypass distinct variable constraints, but I could have missed something. [[User:Kingdon|Kingdon]] 20:08, 12 June 2010 (UTC)

Wikiproofs/T/e/a/Tearoom

@@ -361,4 +361,4 @@ Anyway, I thought I should highlight this development and see if there are any r
 
 :Hi, just to let you know: I'm still watching the changes to the wiki, and, once again, thank you for your contributions. As for your question, I have to admit that, without actually diving into the matter, I'm out of my depth here. I hope someone of the others can help you.--[[User:GrafZahl|GrafZahl]] ([[User talk:GrafZahl|talk]]) 20:27, 23 February 2012 (UTC)
 
-::Thanks for the response. I found that this is (at least roughly) one of the unsolved problems on the metamath site: [http://us.metamath.org/award2003.html#17 17] so I'm hoping I can interest Mr. Megill once I put a few finishing touches on it. [[User:Kingdon|Kingdon]] 05:32, 27 February 2012 (UTC)
+::Thanks for the response. I found that this is (at least roughly) one of the unsolved problems on the metamath site: [http://us.metamath.org/award2003.html#17 17] so I'm hoping I can interest Mr. Megill once I put a few finishing touches on it. [[User:Kingdon|Kingdon]] 05:32, 27 February 2012 (UTC)