Ignore:
Timestamp:
Jun 17, 2011, 6:28:49 PM (8 years ago)
Author:
sacerdot
Message:

More Russell everywhere; getting closer to the goal.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r992 r993  
    13191319      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
    13201320
    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 
    13381321axiom split_elim':
    13391322  ∀A: Type[0].
     
    22252208  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
    22262209 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/
    22372210qed.
    22382211
Note: See TracChangeset for help on using the changeset viewer.