:: Binary Arithmetics. Addition and Subtraction of Integers
:: by Yasuho Mizuhara and Takaya Nishiyama
::
:: Received March 18, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

Lm1: for n being Nat
for p, q being Tuple of n, BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) holds
p = q
proof end;