Ignore:
Timestamp:
Nov 22, 2011, 11:58:43 AM (9 years ago)
Author:
campbell
Message:

Update most of Assembly.ma with new syntax and identifier maps.
Change positive.ma a little to reduce name clashes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/positive.ma

    r1523 r1528  
    217217] qed.
    218218
    219 theorem commutative_plus : commutative ? plus.
     219theorem commutative_plus_pos : commutative ? plus.
    220220#n elim n;
    221221[ #y cases y; normalize; //;
     
    224224
    225225theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m.
    226 #n #m >(commutative_plus (succ n) m)
     226#n #m >(commutative_plus_pos (succ n) m)
    227227<(plus_n_succm …) //; qed.
    228228
     
    775775] qed.
    776776
    777 theorem minus_n_n: ∀n:Pos.one=n-n.
     777theorem minus_n_n_pos: ∀n:Pos.one=n-n.
    778778#n normalize; >(partial_minus_n_n n) //;
    779779qed.
     
    877877qed.
    878878
    879 theorem minus_to_plus :∀n,m,p:Pos.
     879theorem minus_to_plus_pos :∀n,m,p:Pos.
    880880  m < n → n-m = p → n = m+p.
    881881#n #m #p #lemn #eqp applyS plus_minus_m_m; //;
    882882qed.
    883883
    884 theorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p.
     884theorem plus_to_minus_pos :∀n,m,p:Pos.n = m+p → n-m = p.
    885885(* /4/ done in 43.5 *)
    886886#n #m #p #eqp
Note: See TracChangeset for help on using the changeset viewer.