Changeset 3488

Timestamp:

Sep 24, 2014, 3:56:55 PM (5 years ago)

Author:

sacerdot

Message:

One proof repaired.

File:

• LTS/Vm.ma (modified) (4 diffs)

LTS/Vm.ma

@@ -376 +376 @@
                 (λs.match s with [ FINAL ⇒ true | _ ⇒ false])
                 ???.
-@hide_prf cases daemon qed. (*
-[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
+@hide_prf
+[ #s1 #s2 #l
+ cases s1 normalize nodelta [1,2: #abs destruct] -s1 #s1
+ cases s2 normalize nodelta [1: #_ * |2: #_ * #_ #EQ >EQ normalize /2/ ] #s2  
+ inversion(fetch ???) normalize nodelta
   [ #_ #EQ destruct] * normalize nodelta
   [ #seq #lbl #_
@@ -390 +393 @@
   normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
   * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % //
-| #s1 #s2 #l inversion(fetch ???) normalize nodelta
+| #s1 #s2 #l
+  cases s1 normalize nodelta [2: #_ * |3: #s1 ]
+  cases s2 normalize nodelta [1,2,4,5: #abs destruct ] #s2 [2: #_ * #_ /2/ ]
+  inversion(fetch ???) normalize nodelta
   [ #_ #EQ destruct] * normalize nodelta
   [ #seq #lbl #_
@@ -416 +422 @@
   ] 
   whd in ⊢ (??%% → ?); #EQ destruct destruct % //
-|  #s1 #s2 #l inversion(fetch ???) normalize nodelta
+| #s1 #s2 #l
+  cases s1 normalize nodelta [1,2: #abs destruct ] #s1
+  cases s2 normalize nodelta [ #_ * | #_ * /2/ ] #s2
+  inversion(fetch ???) normalize nodelta
   [ #_ #EQ destruct] * normalize nodelta
   [ #seq #lbl #_
@@ -429 +438 @@
   normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_ 
   whd in ⊢ (??%% → ?); #EQ destruct % //
-qed.*)
+qed.
 
 definition asm_concrete_trans_sys ≝