diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-28 17:35:38 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-28 17:35:38 +0100 |
| commit | 4917816d72d131cc0c3a10c00648a5df354e7500 (patch) | |
| tree | d89e4b4e18e797e9a794a34f76349992974db2e5 /src/hls/GiblePargenproofForward.v | |
| parent | 3cca0fa62b1b78ca0df38b539d88704b26b21645 (diff) | |
| download | vericert-4917816d72d131cc0c3a10c00648a5df354e7500.tar.gz vericert-4917816d72d131cc0c3a10c00648a5df354e7500.zip | |
Work on forward proofs
Diffstat (limited to 'src/hls/GiblePargenproofForward.v')
| -rw-r--r-- | src/hls/GiblePargenproofForward.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 6411351..cf81802 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -324,7 +324,9 @@ all be evaluable. forall pred f, predicated_not_in_forest pred f = true -> forall x, predicated_not_inP pred (f #r x). - Proof. Admitted. + Proof. + unfold predicated_not_in_forest, predicated_not_in_pred_expr; intros. + eapply andb_prop in H. inv H. Lemma pred_not_in_forest_exitP : forall pred f, |