Changeset 3592
- Timestamp:
- Jul 25, 2015, 6:09:09 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/variable_stack_pass.ma
r3590 r3592 474 474 var_instr_bond_ok st (SEQ … seq opt_l i) ct → 475 475 var_instr_bond_ok st i ct. 476 * [|#x #xs]#i #seq #ol #ct whd in ⊢(%→?);476 #act_frm (* [|#x #xs]*) #i #seq #ol #ct whd in ⊢(%→?); 477 477 <(append_nil … [?]) >divide_continuation_on_frame_app 478 478 inversion(divide_continuation_on_frames ct ?) 479 normalize nodelta [2,4: #y #ys #_] #EQdivide 480 [1,3:#ABS cases ABS 481 |2,4: 482 ** * [2,4:#m #Hm] #H2 #H3 whd in match(var_instr_bond_ok ???); 483 inversion (divide_continuation_on_frames ct [i]) normalize nodelta 484 <(append_nil … [?]) >divide_continuation_on_frame_app 485 >EQdivide normalize nodelta /2 by absurd/ 486 #lfi #llfi #H9 #H10 destruct % 487 [1,3,5,7: % 488 [1,3,5,7: 489 |2,4,6,8: /2 by / 490 ] 491 |2,4,6,8: 492 ] 493 494 ] 495 496 497 498 (* 499 [2: #H1 #H2 #H3 #H4|3:#H] [1,2:#ABS cases ABS] 500 cases i whd in match(var_instr_bond_ok ??); inversion(ct) 501 [1,3,5,7: whd in match(var_instr_bond_ok ???);] 502 [#_ whd in match(divide_continuation_on_frames ??); 503 #ABS destruct| #H1 #H2 whd in match (divide_continuation_on_frames ??); 504 #ABS destruct| #H1 #H2 #H3 #H4 whd in match (divide_continuation_on_frames ??); #ABS destruct 505 |#H8 #H9 #H10 #H11 #H12 #H13 #H14 whd in match (divide_continuation_on_frames ??); #ABS destruct 506 |* #fl #fi #H10 cases fl [#fn #ccl|2,3:#op] #H20 [2,3:#H21 whd in match (divide_continuation_on_frames ??); 507 #ABS destruct|whd in match (divide_continuation_on_frames ??); 508 #H29 cases H10 [2:#al #l] whd in match (divide_continuation_on_frames ??); 509 [2:#ABS destruct 510 |1: whd in match(var_instr_bond_ok …); 511 ] 512 ] 513 ] 514 *) 479 normalize nodelta [2,4: #x #xs #_] #EQdivide 480 481 cases act_frm -act_frm [2,4: #y #ys] ** 482 #H1 #H2 #H3 whd in match (var_instr_bond_ok ???); 483 <(append_nil … [?]) >divide_continuation_on_frame_app >EQdivide normalize nodelta 484 % // % // 515 485 cases daemon 516 486 qed.
Note: See TracChangeset
for help on using the changeset viewer.