 Timestamp:
 Sep 22, 2011, 6:03:03 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1251 r1256 375 375 ]. 376 376 377 axiom Sm_leq_n_m_leq_n: 378 ∀m, n: nat. 379 S m ≤ n → m ≤ n. 380 381 let rec mapi_aux 382 (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat) 383 on n: n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → BitVectorTrie b n ≝ 384 match n return λn. n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → BitVectorTrie b n with 385 [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16. 386 match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with 387 [ Leaf l ⇒ λprf. Leaf … (f accu l) 388  Stub s ⇒ λprf. Stub … s 389  Node n' l r ⇒ λabsrd. ⊥ 390 ] (refl … 0) 391  S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16  (S n')). 392 match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with 393 [ Leaf l ⇒ λabsrd. ⊥ 394  Stub s ⇒ λprf. Stub … s 395  Node n'' l r ⇒ λprf. 396 Node ? n'' ? ? 397 (* (mapi_aux a b f n' ? (l⌈n'' ↦ n'⌉) ((false ::: accu)⌈S (16  S n') ↦ 16  n'⌉)) 398 (mapi_aux a b f n' ? (r⌈n'' ↦ n'⌉) ((true ::: accu)⌈S (16  S n') ↦ 16  n'⌉))*) 399 ] (refl ? (S n')) 400 ]. 401 [ 1,2: destruct(absrd) 402  3 : destruct(prf) 403 @(mapi_aux a b f n' ? l ((false ::: accu)⌈S (16  S n') ↦ 16  n'⌉)) 404 [ 1: @Sm_leq_n_m_leq_n 405 assumption 406  2: <minus_Sn_m 407 [ 1: >minus_S_S % 408  2: assumption 409 ] 410 ] 411  4 : destruct(prf) 412 @(mapi_aux a b f n' ? r ((true ::: accu)⌈S (16  S n') ↦ 16  n'⌉)) 413 [ 1: @Sm_leq_n_m_leq_n 414 assumption 415  2: <minus_Sn_m 416 [ 1: >minus_S_S % 417  2: assumption 418 ] 419 ] 420 ] 421 qed. 422 423 check mapi_aux. 424 377 425 definition translate_internal ≝ 378 426 λglobals. 379 427 λint_fun. 380 let uses ≝ examine_internal globals int_fun in ?. 428 let uses ≝ examine_internal globals int_fun in 429 let 381 430 382 431 definition translate_funct ≝
Note: See TracChangeset
for help on using the changeset viewer.