Loading theory "HOL-Corec_Examples.Iterate_GPV"
Loading theory "HOL-Corec_Examples.LFilter"
Loading theory "HOL-Corec_Examples.Simple_Nesting"
Loading theory "HOL-Corec_Examples.Stream_Processor"
Loading theory "HOL-Corec_Examples.Paper_Examples"
### Introduced fixed type variable(s): 'b in "P__" or "x__" or "xs__"
### theory "HOL-Corec_Examples.LFilter"
### 3.901s elapsed time, 23.168s cpu time, 1.620s GC time
*** Failed to finish proof (line 44 of "~~/src/HOL/Corec_Examples/Stream_Processor.thy"):
*** goal (1 subgoal):
***  1. \<And>s x1. x1 (shd s) = Get x1 \<Longrightarrow> False
### theory "HOL-Corec_Examples.Iterate_GPV"
### 10.790s elapsed time, 62.660s cpu time, 10.620s GC time
### theory "HOL-Corec_Examples.Stream_Processor"
### 12.250s elapsed time, 71.488s cpu time, 11.092s GC time
*** Failed to finish proof (line 67 of "~~/src/HOL/Corec_Examples/Stream_Processor.thy"):
*** goal (1 subgoal):
***  1. \<And>x1 x21 x22.
***        \<lbrakk>(x22, In (Put x21 x22)) \<notin> map_prod In In ` sub; x1 x21 = Get x1\<rbrakk>
***        \<Longrightarrow> False
### theory "HOL-Corec_Examples.Simple_Nesting"
### 26.818s elapsed time, 126.112s cpu time, 14.760s GC time
### theory "HOL-Corec_Examples.Paper_Examples"
### 38.857s elapsed time, 151.204s cpu time, 16.400s GC time
*** Failed to finish proof (line 67 of "~~/src/HOL/Corec_Examples/Stream_Processor.thy"):
*** goal (1 subgoal):
***  1. ⋀x1 x21 x22.
***        ⟦(x22, In (Put x21 x22)) ∉ map_prod In In ` sub; x1 x21 = Get x1⟧
***        ⟹ False
*** At command "by" (line 66 of "~~/src/HOL/Corec_Examples/Stream_Processor.thy")
*** Failed to finish proof (line 44 of "~~/src/HOL/Corec_Examples/Stream_Processor.thy"):
*** goal (1 subgoal):
***  1. ⋀s x1. x1 (shd s) = Get x1 ⟹ False
*** At command "by" (line 43 of "~~/src/HOL/Corec_Examples/Stream_Processor.thy")