Changeset 1600 for src/ASM/Status.ma
 Timestamp:
 Dec 13, 2011, 1:41:08 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r1599 r1600 6 6 include "ASM/Arithmetic.ma". 7 7 include "ASM/BitVectorTrie.ma". 8 include " ASM/JMCoercions.ma".8 include "basics/russell.ma". 9 9 10 10 definition Time ≝ nat. … … 785 785 786 786 lemma set_arg_16_ok: ∀M,s,v,x. clock M s = clock … (set_arg_16 M s v x). 787 #M #s #x #v whd in match set_arg_16; normalize nodelta @ sig2787 #M #s #x #v whd in match set_arg_16; normalize nodelta @pi2 788 788 qed. 789 789 … … 926 926 927 927 lemma set_arg_8_ok: ∀M,s,x,v. clock M s = clock … (set_arg_8 M s x v). 928 #M #s #x #v whd in match set_arg_8; normalize nodelta @ sig2928 #M #s #x #v whd in match set_arg_8; normalize nodelta @pi2 929 929 qed. 930 930 … … 1084 1084 1085 1085 lemma set_arg_1_ok: ∀M,s,x,v. clock M s = clock … (set_arg_1 M s x v). 1086 #M #s #x #v whd in match set_arg_1; normalize nodelta @ sig21086 #M #s #x #v whd in match set_arg_1; normalize nodelta @pi2 1087 1087 qed. 1088 1088
Note: See TracChangeset
for help on using the changeset viewer.