@@ -561,45 +561,45 @@ <h2><a class="toc-backref" href="#id5" role="doc-backlink">Variant: <code class=
561561 } ,
562562 {
563563 "goals" :[
564- "Type variables: <none>\n\n------------------------------------------------------------------------\npre = Rpbar. '0\n\n M.f \n\npost = (! 0 <= res)%xr\n"
564+ "Type variables: <none>\n\n------------------------------------------------------------------------\npre = '0\n\n M.f \n\npost = (! 0 <= res)%xr\n"
565565 ] ,
566566 "message" :""
567567 } ,
568568 {
569569 "goals" :[
570- "Type variables: <none>\n\n------------------------------------------------------------------------\npre = Rpbar. '0\n\n M.f \n\npost = (! 0 <= res)%xr\n"
570+ "Type variables: <none>\n\n------------------------------------------------------------------------\npre = '0\n\n M.f \n\npost = (! 0 <= res)%xr\n"
571571 ] ,
572572 "message" :""
573573 } ,
574574 {
575575 "goals" :[
576- "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = Rpbar. '0\n\n(1--) if (x < 0) { \n(1.1) y <- -x \n(1--) } else { \n(1?1) y <- x \n(1--) } \n\npost = (! 0 <= y)%xr\n"
576+ "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = '0\n\n(1--) if (x < 0) { \n(1.1) y <- -x \n(1--) } else { \n(1?1) y <- x \n(1--) } \n\npost = (! 0 <= y)%xr\n"
577577 ] ,
578578 "message" :""
579579 } ,
580580 {
581581 "goals" :[
582- "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = (x < 0) `|` Rpbar. '0\n\n(1) y <- -x \n\npost = (! 0 <= y)%xr\n" ,
583- "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = (! x < 0) `|` Rpbar. '0\n\n(1) y <- x \n\npost = (! 0 <= y)%xr\n"
582+ "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = (x < 0) `|` '0\n\n(1) y <- -x \n\npost = (! 0 <= y)%xr\n" ,
583+ "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = (! x < 0) `|` '0\n\n(1) y <- x \n\npost = (! 0 <= y)%xr\n"
584584 ] ,
585585 "message" :""
586586 } ,
587587 {
588588 "goals" :[
589- "Type variables: <none>\n\n------------------------------------------------------------------------\nforall &hr, (! 0 <= -x{hr})%xr <= (x{hr} < 0) `|` Rpbar. '0\n" ,
590- "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = (! x < 0) `|` Rpbar. '0\n\n(1) y <- x \n\npost = (! 0 <= y)%xr\n"
589+ "Type variables: <none>\n\n------------------------------------------------------------------------\nforall &hr, (! 0 <= -x{hr})%xr <= (x{hr} < 0) `|` '0\n" ,
590+ "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = (! x < 0) `|` '0\n\n(1) y <- x \n\npost = (! 0 <= y)%xr\n"
591591 ] ,
592592 "message" :""
593593 } ,
594594 {
595595 "goals" :[
596- "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = (! x < 0) `|` Rpbar. '0\n\n(1) y <- x \n\npost = (! 0 <= y)%xr\n"
596+ "Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = (! x < 0) `|` '0\n\n(1) y <- x \n\npost = (! 0 <= y)%xr\n"
597597 ] ,
598598 "message" :""
599599 } ,
600600 {
601601 "goals" :[
602- "Type variables: <none>\n\n------------------------------------------------------------------------\nforall &hr, (! 0 <= x{hr})%xr <= (! x{hr} < 0) `|` Rpbar. '0\n"
602+ "Type variables: <none>\n\n------------------------------------------------------------------------\nforall &hr, (! 0 <= x{hr})%xr <= (! x{hr} < 0) `|` '0\n"
603603 ] ,
604604 "message" :""
605605 } ,
0 commit comments