Mental Arithmetic
By Richard Weyhrauch
December 25, 2015

This note is called: [MENTAL-ARITHMETIC]
The notation used in this note is described in [NOTATION]
Under development

Preface

This note gives a theory of Mental arithmetic. The issue addressed here is what do we know about arithmetic and how we can reason about natural numbers.

Introduction

Googel ...

The Theory of Mental Arithmetic

Objects in a head of type [natnum] (natural numbers starting with 0, as is customary in computer science) are ...

Small [natnum]s
large [natnum]s

computer arithmetic

(ISIN n c)
(IMPLIES (AND (gt n 0) (ISIN n c)) (ISIN (pred n) c))
(list-length (l) 
  (IF (EQUAL l EmptyList) 0 (succ (list-lendth (list-rest l)))) )
(IMPLIES (ISIN l c) (ISIN (list-length l) c))
(IMPLIES (ISIN n c) (lt (size n) (size c)) )
(EXIST n (NOT (ISIN n c)))
(IMPLIES (gt (size (+ x y)) (size c)) (NOT (ISIN (+ x y) c)) )653182012566