Changeset 2316 for src/ASM/Policy.ma


Ignore:
Timestamp:
Sep 3, 2012, 9:03:24 AM (7 years ago)
Author:
boender
Message:
  • committed temporary version: true version has to wait until I recuperate my hard disk
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2264 r2316  
    186186  policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
    187187    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
    188 #program #n #Heq cases daemon (* XXX *)
     188#program #n #Heq inversion (jump_expansion_internal program n) #x cases x -x
     189 #no_ch #pol cases pol normalize nodelta
     190 [ #H #Hj lapply (step_none program n) >Hj #Hn lapply (Hn (refl ??) 1) <plus_n_Sm <plus_n_O
     191   #HSeq >HSeq lapply (Hn (refl ??) 2) <plus_n_Sm <plus_n_Sm <plus_n_O #HSSeq >HSSeq / by /
     192 | -pol #pol #Hpol #Hn >Hn in Heq; whd in match (policy_equal_opt ???);
     193   lapply (refl ? (jump_expansion_internal program (S n)))
     194   whd in match (jump_expansion_internal program (S n)) in ⊢ (???% → ?); >Hn
     195   normalize nodelta inversion no_ch #Hno_ch normalize nodelta #Seq >Seq
     196   [ #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
     197     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
     198     normalize nodelta #Teq >Teq @pe_refl
     199   | #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
     200     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
     201     normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq; (*320s*)
     202     #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol
     203     [ normalize nodelta #HSn #Heq #Seq cases Heq
     204     | -Spol #Spol normalize nodelta cases Sno_ch normalize nodelta #HSn #Heq #Seq
     205       [ @pe_refl
     206       | cases daemon
     207       ]
     208     ]
     209   ]
     210 ]
    189211qed.
    190212
     
    445467          [ lapply (jump_pc_equal program (2*|program|))
    446468            >Feq >Geq normalize nodelta #H @H @Heq
     469          | @Heq
    447470          | cases daemon (* true, but have to add this to properties *)
     471          | cases daemon
    448472          | @(proj2 ?? (proj1 ?? HGp))
    449473          ]
Note: See TracChangeset for help on using the changeset viewer.