Changeset 3590


Ignore:
Timestamp:
Jul 20, 2015, 6:34:11 PM (4 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3589 r3590  
    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 ⊢(%→?); inversion(divide_continuation_on_frames ct ?)
    477 normalize nodelta [2: #H1 #H2 #H3 #H4|3:#H] [1,2:#ABS cases ABS]
     476* [|#x #xs] #i #seq #ol #ct whd in ⊢(%→?);
     477<(append_nil … [?]) >divide_continuation_on_frame_app
     478inversion(divide_continuation_on_frames ct ?)
     479normalize 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 ???);
     483inversion (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]
    478500cases i whd in match(var_instr_bond_ok ??); inversion(ct)
    479501[1,3,5,7: whd in match(var_instr_bond_ok ???);]
     
    490512]
    491513]
    492 
     514*)
    493515cases daemon
    494516qed.
     
    9881010  #s2' * #s2'' * #s2''' * #t1 * #exe' * #t3 *** #rel' #sil1 #sil2 #HR
    9891011  %{s2'} %{s2''} %{s2'''} %{t1} %{exe'} %{t3} % [ % [%] ] assumption
    990 |*: cases daemon (*todo per giulio*)
    991 ]
    992 qed.
     1012|*: (*todo per giulio*)
     1013#OsFsp #OsSsp #OsFsp' #NFLfl #AEfl #ACfl #ACfl' #SRfl
     1014%{?} [1,3: /2 by /
     1015|*: % [1,3: /2 by /
     1016|*: % [1,3: /2 by t_base/
     1017|*: % [2,4: %
     1018          [1,3: %
     1019                [1,3: %
     1020                    [1,3: %
     1021                        [1,3: %
     1022                            [1,3: % whd in AEfl;
     1023                            ]
     1024                        ]
     1025                    ]
     1026                 ]
     1027             ]
     1028         ]
     1029 ]
     1030 ]
     1031 ]
     1032cases daemon (*todo per giulio*)
     1033]
     1034qed.
Note: See TracChangeset for help on using the changeset viewer.