diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-10 14:12:45 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-10 14:12:45 +0100 |
| commit | 67ba392ddddef079f7ed2e04b266b1b0029f1bf5 (patch) | |
| tree | 8dd215410ce1170b1cb12f486c61aa769e6c3690 | |
| parent | 243c5b07c29c8636d7089d03ee5f9c58beaf9fda (diff) | |
| download | vericert-67ba392ddddef079f7ed2e04b266b1b0029f1bf5.tar.gz vericert-67ba392ddddef079f7ed2e04b266b1b0029f1bf5.zip | |
Try to prove main theorem
Missing some link between forests
| -rw-r--r-- | src/hls/GiblePargenproof.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 90c132c..d9436b5 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -853,6 +853,11 @@ have been evaluable. (* { inv H. inv H8. exists pr'. intros x0. specialize (H x0). auto. } *) simplify. exploit abstr_seq_reverse_correct; eauto. + { inv H8. inv H14. + eapply check_evaluability1_evaluable. + eauto. eauto. + eapply abstract_sequence_evaluable. + } admit. admit. reflexivity. simplify. exploit seqbb_step_parbb_step; eauto; intros. econstructor; split; eauto. |