equal
deleted
inserted
replaced
1731 @{term "bs @ retrieve (fuse [Z] (bder c r)) v1 @ retrieve (ASTAR [] r) (Stars vs)"} |
1731 @{term "bs @ retrieve (fuse [Z] (bder c r)) v1 @ retrieve (ASTAR [] r) (Stars vs)"} |
1732 \] |
1732 \] |
1733 We can move out the @{term "fuse [Z]"} and then use the IH to show that left-hand side |
1733 We can move out the @{term "fuse [Z]"} and then use the IH to show that left-hand side |
1734 and right-hand side are equal. This completes the proof. |
1734 and right-hand side are equal. This completes the proof. |
1735 \end{proof} |
1735 \end{proof} |
|
1736 |
|
1737 |
|
1738 |
|
1739 \bibliographystyle{plain} |
|
1740 \bibliography{root} |
|
1741 |
1736 \<close> |
1742 \<close> |
1737 |
|
1738 |
|
1739 |
|
1740 (*<*) |
1743 (*<*) |
1741 end |
1744 end |
1742 (*>*) |
1745 (*>*) |