Dear Members, Following is a proof using the SUM operator for an arbritary number of constants: http://www.dcproof.com/SUMconstants.proof (DC Proof format) ...
Effective immeidately... New version of DC Proof 1.0 dated 2005-08-5 includes 1. New shortcuts for SUM and PROD operators (on Numbers menu) 2. Minor bug fixes,...
Dear members, I received the following proof from Mark Hurd. Using the new SUM shortcut, he proved that x + x^2 + x^3 + ... + x^k = x*((x^k-1)/(x-1)) for x>1 ...
Effective immediately... New release of DC Proof 1.0 dated 2005-8-8 includes: 1. Improved graphics (screen shots) in tutorial and user guide. 2. Larger fonts...
Effective immediately New release of DC Proof 1.0 dated 2005-12-10 Includes: 1. Fixed definition of pairwise intersection generated by Set Operations option. ...
Effective Immediately New Release of DC Proof 1.0 Includes: 1. Fixed bug in Universal Specification form that caused the form to close in response to some...
Dear members, Here is another, considerably simpler approach to working with real numbers in DC Proof. Rather than constructing the reals starting with Peano's...
Effective Immediately New Release of DC Proof 1.0 dated 2006-02-07 Includes: 1. Changed colour of system generated comments on main screen and in HTML output...
Effectively Immediately New release of DC Proof 1.0 dated 2006-02-15 includes: 1. Fixed bug in Subset Rule that could lead to invalid proofs as a result of...
Here are the axioms for the real numbers that users of DC Proof may find useful for doing proofs in real analysis (calculus). I will include it in the Samples...
Effective Immediately New Release of DC Proof 1.0 Dated 2006-02-22 Includes: 1. Fixed bug in Subset Rule that would sometimes insert brackets improperly....
Effective Immediately New Release of DC Proof 1.0 includes: 1. Warning on Premise Rule that lists existential variables (those introduced by Existential...
Effectively Immediately New release of DC Proof 1.0 dated 2006-03-10 includes: 1. In insert mode, after Undoing a change, cursor now properly reset at insert...
Effective Immediately New Release of DC Proof 1.0 dated 2006-03-20 includes: 1. Added Reset button to Substitution Form. 2. When closing a Premise Block...
Effective Immediately New release of DC Proof 1.0 dated 2006-05-26 Includes: 1. Improved warning message for the Premise Rule indicating any relevant...
Effective Immedidately New Release of DC Proof 1.0 dated 2006-08-14 includes: 1. Minor changes to Tutorial in User Documentation. No changes to functionality. ...
Hi list, looking at the proof regarding addition of natural numbers, it was stated that the subset rule had been used-- in particular the set s being...
Thomas, Thanks for bringing this to my attention! The proof in question (at the DC Proof website) was written with an old version of DC Proof. Currently,...
Hi Dan, here's a fragment of a proof. Applying the uspec/espec rule to line 94, I get the warning: "x will depend on: x1, x2, y1, y2." Note that none of these...
Hi Thomas, You will get that message sometimes when you do Existential Specification. It is for informational purposes only to help you understand warnings...
Hi folks, I'd like to prove for all natural numbers a,b that a +a=b+b implies a=b. My ideas so far: Having shown that a<b, a=b, b<a are mutually exclusive, it...
Hi Thomas, Heading in the direction you've suggested: x<y =>x+x<y+x =>x+y<y+y x+y=y+x =>x+x<y+y This requires a<b=>a+c<b+c, a+b=b+a, a<b & b<c => a<c And if...
Hi list, there's something odd about substitution: Suppose you have r=c+a+b and x=a+b then substituting x in the 1st equation is impossible; whereas it works...
Hi Thomas, The usual order precedence for algebraic operators is built into DC Proof. In this case r=c+a+b is interpreted as r=(c+a)+b, the left- most +...
Effectively immediately New release of DC Proof 1.0 includes: 1. Change to User Reference Guide. Added note to section on Substitution Rule: "Please note that...
