Changeset 2316 for src/ASM/Policy.ma

Timestamp:

Sep 3, 2012, 9:03:24 AM (8 years ago)

Author:

boender

Message:

• committed temporary version: true version has to wait until I recuperate my hard disk

File:

• src/ASM/Policy.ma (modified) (2 diffs)

src/ASM/Policy.ma

@@ -186 +186 @@
   policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
     (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
-#program #n #Heq cases daemon (* XXX *)
+#program #n #Heq inversion (jump_expansion_internal program n) #x cases x -x
+ #no_ch #pol cases pol normalize nodelta
+ [ #H #Hj lapply (step_none program n) >Hj #Hn lapply (Hn (refl ??) 1) <plus_n_Sm <plus_n_O
+   #HSeq >HSeq lapply (Hn (refl ??) 2) <plus_n_Sm <plus_n_Sm <plus_n_O #HSSeq >HSSeq / by /
+ | -pol #pol #Hpol #Hn >Hn in Heq; whd in match (policy_equal_opt ???);
+   lapply (refl ? (jump_expansion_internal program (S n)))
+   whd in match (jump_expansion_internal program (S n)) in ⊢ (???% → ?); >Hn
+   normalize nodelta inversion no_ch #Hno_ch normalize nodelta #Seq >Seq
+   [ #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
+     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
+     normalize nodelta #Teq >Teq @pe_refl
+   | #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
+     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
+     normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq; (*320s*)
+     #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol
+     [ normalize nodelta #HSn #Heq #Seq cases Heq
+     | -Spol #Spol normalize nodelta cases Sno_ch normalize nodelta #HSn #Heq #Seq
+       [ @pe_refl
+       | cases daemon
+       ]
+     ]
+   ]
+ ]
 qed.
 
@@ -445 +467 @@
           [ lapply (jump_pc_equal program (2*|program|))
             >Feq >Geq normalize nodelta #H @H @Heq
+          | @Heq
           | cases daemon (* true, but have to add this to properties *)
+          | cases daemon
           | @(proj2 ?? (proj1 ?? HGp))
           ]