Changeset 3592


Ignore:
Timestamp:
Jul 25, 2015, 6:09:09 PM (4 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3590 r3592  
    474474var_instr_bond_ok st (SEQ … seq opt_l i) ct →
    475475var_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 ⊢(%→?);
    477477<(append_nil … [?]) >divide_continuation_on_frame_app
    478478inversion(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 *)
     479normalize nodelta [2,4: #x #xs #_] #EQdivide
     480
     481cases 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% // % //
    515485cases daemon
    516486qed.
Note: See TracChangeset for help on using the changeset viewer.