Email Gateway (Aug 18 2022 at 17:45): Email Gateway (Aug 18 2022 at 17:45):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi all,
have the following weird behaviour. After having applied auto on my goal, I am
left with 24 subgoals. Applying 24 copies of the following invokation of the
blast method solves all 24 subgoals. However, if I try to collaspe all of them
into a single invokation apply(blast 25 ...)+, I get the exception below.
What is going wrong here? And how can I fix it?
If need be, I can make my theories available, but I doubt that I can produce a
minimal core example.
apply(blast 25 intro: rtranclp_trans rtranclp_tranclp_tranclp
treds1r_cons_treds1r List1Red2 treds1t_cons_treds1t
dest: t)
*** exception THM 1 raised (line 212 of "conv.ML"):
*** gconv_rule
*** EX es'' xs''.
*** P,e # es,n,h' |- (es'', xs'') [<-->] (stk', loc', pc', xcp') &
*** (if tmoves2 (compP2 P) h stk (e # es) pc xcp
*** then h' = h &
*** (if xcp' = Any --> pc < pc' then treds1r else treds1t) P t h
*** (e' # es, xs) (es'', xs'')
*** else EX ta' es' xs'.
*** treds1r P t h (e' # es, xs) (es', xs') &
*** P,t |- <<es',(h, xs')>> [-ta'->] <<es'',(h', xs'')>> &
*** ta_bisim wbisim1 (extTA2J1 P ta') ta &
*** ¬ tmoves1 P h es' &
*** (calls1 (e' # es) = None &
*** no_calls2 (e # es) pc & es' = e' # es & xs' = xs))
*** At command "apply"
Best regards,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC