Changeset 3591 for LTS/Vm.ma


Ignore:
Timestamp:
Jul 20, 2015, 7:08:44 PM (4 years ago)
Author:
piccolo
Message:

stared pass stack to monostack, closed the first three proof obbligations of simulation conditions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3563 r3591  
    829829[ #st #l #prf  #t' normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
    830830#s1 #s2 #s3 #l1 #prf1 #t2 #l2 #prf2 #t3 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    831 qed.
    832 
    833 let rec chop (A : Type[0]) (l : list A) on l : list A ≝
    834 match l with
    835 [ nil ⇒ nil ?
    836 | cons x xs ⇒ match xs with [ nil ⇒ nil ? | cons _ _ ⇒ x :: chop … xs]
    837 ].
    838 
    839 lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l.
    840 #A #x #l elim l normalize // #y * normalize //
    841 qed.
    842 
    843 lemma chop_mem : ∀A : Type[0].∀x : A.∀l : list A. mem … x (chop ? l) → mem … x l.
    844 #A #x #l elim l [*] #y * [ normalize /2/] #z #zs #IH * [/2/] /3/
    845831qed.
    846832
Note: See TracChangeset for help on using the changeset viewer.