Changeset 993 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 17, 2011, 6:28:49 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r992 r993 1319 1319 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi. 1320 1320 1321 axiom pair_elim':1322 ∀A,B,C: Type[0].1323 ∀T: A → B → C.1324 ∀p.1325 ∀P: A×B → C → Prop.1326 (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →1327 P p (let 〈lft, rgt〉 ≝ p in T lft rgt).1328 1329 axiom pair_elim'':1330 ∀A,B,C,C': Type[0].1331 ∀T: A → B → C.1332 ∀T': A → B → C'.1333 ∀p.1334 ∀P: A×B → C → C' → Prop.1335 (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →1336 P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).1337 1338 1321 axiom split_elim': 1339 1322 ∀A: Type[0]. … … 2225 2208 \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). 2226 2209 cases daemon. 2227 qed.2228 2229 lemma pair_destruct_1:2230 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.2231 #A #B #a #b *; /2/2232 qed.2233 2234 lemma pair_destruct_2:2235 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.2236 #A #B #a #b *; /2/2237 2210 qed. 2238 2211
Note: See TracChangeset
for help on using the changeset viewer.