Ignore:
Timestamp:
Nov 19, 2011, 12:38:36 AM (9 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

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

    r891 r1517  
    237237   |#m cases z
    238238      [//
    239       |#p apply transitive_lt (* XXX: auto??? *)
     239      |#p @transitive_lt (* XXX: auto??? *)
    240240      |//]
    241241   |#m #Hl cases Hl]
     
    249249   |#m cases z
    250250      [1,2://
    251       |#p #Hl #Hr apply (transitive_lt … Hr Hl)]
     251      |#p #Hl #Hr @(transitive_lt … Hr Hl)]
    252252   ]
    253253]
     
    463463   [//
    464464   |//
    465    |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
     465   |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n
    466466      cases (pos_compare q p);//]
    467467|#p cases y
    468468   [//;
    469    |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
     469   |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n
    470470      cases (pos_compare q p);//
    471471   |normalize;//]
     
    503503  ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
    504504#n #m
    505 whd in ⊢ (??%%) 
     505whd in ⊢ (??%%);
    506506<(pos_compare_S_S …)
    507507>(minus_S_S …)
     
    522522[ //;
    523523| #m' >Zpred_pos_succ
    524     change in ⊢ (??(??%)?) with (Zsucc (pos m'))
     524    change in ⊢ (??(??%)?); with (Zsucc (pos m'))
    525525    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
    526 | #m' whd in ⊢ (??%%) >pos_compare_S_one normalize;
     526| #m' whd in ⊢ (??%%); >pos_compare_S_one normalize;
    527527    >partial_minus_S_one normalize; >pos_nonzero
    528528    <pred_succ_n //
    529 | #m' #n' whd in ⊢ (??%%) <pos_compare_S_S
     529| #m' #n' whd in ⊢ (??%%); <pos_compare_S_S
    530530    >minus_S_S
    531531    >minus_S_S normalize
     
    601601
    602602lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
    603 #n #m whd in ⊢ (??%%) <pos_compare_S_S
     603#n #m whd in ⊢ (??%%); <pos_compare_S_S
    604604>minus_S_S >minus_S_S
    605605 //; qed.
     
    676676#x #y cases x
    677677[cases y;//
    678 |*:#n cases y;//;#m whd in ⊢ (??(?%)%) @pos_compare_elim normalize;//]
     678|*:#n cases y;//;#m whd in ⊢ (??(?%)%); @pos_compare_elim normalize;//]
    679679qed.
    680680
     
    686686#x cases x
    687687[//
    688 |*:#n whd in ⊢ (??%?) >pos_compare_n_n //]
     688|*:#n whd in ⊢ (??%?); >pos_compare_n_n //]
    689689qed.
    690690
Note: See TracChangeset for help on using the changeset viewer.