Changeset 2668 for src/Clight


Ignore:
Timestamp:
Feb 15, 2013, 11:27:56 AM (8 years ago)
Author:
campbell
Message:

Intermediate measurable proof check-in before I change its traces again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/trivial.test.ma

    r2645 r2668  
    113113example ms :
    114114 let 〈p0,init〉 ≝ clight_label myprog in
    115  measurable Clight_pcs p0 1 4 (λfn. 1) 1.
     115 measurable Clight_pcs p0 0 4 (λfn. 1) 1.
    116116whd whd in match (state ????);
    117 % [2: % [2: % [2: % [2:
     117% [2: % [2: % [2: % [2: % [2:
    118118@poke
    119119[ @poke
    120120  [ @poke
    121121    [ @poke
    122       [ whd in ⊢ (??%?); %
    123       | whd in ⊢ (??%? → ??%?); #E destruct %
     122      [ @poke
     123        [ %
     124        | whd in ⊢ (??%? → ??%?); #E destruct %
     125        ]
     126      | * #E1 #E2 whd in E1:(??%?); destruct whd in E2:(??%?); destruct %
    124127      ]
    125     | * #E1 #E2 whd in E1:(??%?); destruct whd in E2:(??%?); destruct
     128    | * * #E1 #E2 #E3 whd in E1:(??%?); destruct whd in E2:(??%?); destruct whd in E3:(??%?); destruct
    126129      whd %[2: % [2: %{[?]} [2: %[2: %[2: %[2: %[ %[ % | whd % ]| whd in ⊢ (??%?); % ]
    127130      |skip]|skip]|skip]|skip]|skip]|skip]
    128131    ]
    129   | * * #E1 #E2 #_ whd in E1:(??%?); destruct whd in E2:(??%?); destruct
     132  | * * * #E1 #E2 #E3 #_ whd in E1:(??%?); destruct whd in E2:(??%?); destruct whd in E3:(??%?); destruct
    130133    whd %
    131134  ]
    132 | * * * #E1 #E2 #_ #_ whd in E1:(??%?); destruct whd in E2:(??%?); destruct
     135| * * * * #E1 #E2 #E3 #_ #_ whd in E1:(??%?); destruct whd in E2:(??%?); destruct whd in E3:(??%?); destruct
    133136  whd in ⊢ (?%?); //
    134137] qed.
Note: See TracChangeset for help on using the changeset viewer.