我说：如果我制作一个有向图 G，每个顶点恰好有一个出度和任意数量的入度，那么

1) 图最多可以有 1 个循环
2) 图 G 是连通的

如果不正确，也请提供一个反例。

如果为真，您能否提出更多可用于消除循环的图 G 属性？（注意：新顶点动态加入和离开）

我正在尝试使用 ESP32 模块为无线网络制作分散的网格形成算法。
每个有向出边都是一个连接 AP（接入点）的 STA（站）
每个顶点都是一个节点

我正在使用 bookdown 来输入我的一些数学课程的笔记。我想使用此处描述的定理和证明，但是当我实际编写 .pdf 文件时，我遇到了渲染问题。基本上，.pdf 呈现看似代码的内容，但实际上没有正确格式化，因为我可以在 LaTeX 中“手动”执行。

我尝试在输出之间切换（HTML 和 .pdf 编织物都有相同的问题），我曾经devtools::install_github('rstudio/bookdown')安装过 bookdown 的开发版本，并且我已经按照以下链接进行操作，但无济于事：here和here这是一个简单的错误，我确定我已经处理好了。

这是我的标题：

这是我尝试过的

编辑：我也试过直接粘贴这里的例子，但没有运气。

如前所述，我期待此页面上出现类似 Theorem 2.1 的内容，但它打印的内容看起来像代码。我在这里上传了一个示例，如果我切换到 HTML，也会发生同样的事情。

序幕

我们要计算模幂A ^{(B C)} mod p = ?，其中A, B, C, 和p是已知的，p是一个素数。例如：2 ^{4 3}模 23 = 6

如果我们直接计算，首先 B ^C = e，然后 A ^e = n，最后 n mod p；我们将遇到为 e 和 n 创建（可能）非常大的中间结果的问题。例如：e = 4 ³ = 64，n = 2 ⁶⁴ ≈ 1.845x10 ¹⁹，最后是 n mod 23 = 6

然而，以直接的方式做这件事，我们没有利用 p 是一个素数并且我们正在做模幂运算的事实。而且这样做，我们将在时间（CPU）和空间（内存）方面遇到使用计算机程序计算结果的问题。

（是的，我们可以通过首先将 A ^{(B C)} mod p 减少到 A ^e模式 p 来使用恒等式进行快速模幂运算。例如 A ² mod p = (A ⋅ A) mod p = [(A mod p) ⋅ (A mod p)] mod p – 但这不是我们想要的）。(a ⋅ b) mod m = [(a mod m) ⋅ (b mod m)] mod m

聪明的方法——使用费马小定理

正如GeeksforGeeks上的 Find power of power under mod of a prime和这个问题的起源中所记录的那样，我们在 A ^{(B C)} mod p 中的指数 B ^C可以使用费马小定理以不同方式表示。

费马小定理：如果 p 是素数，则a ^{(p - 1) ≡ 1 (mod p)}

导致以下转变：

1. 可以将指数 B ^C重写为 x ⋅ (p - 1) + y

2. 使用该替代表达式，我们的 A ^{B C}变为 A ^{x ⋅ (p - 1) + y} = A ^{x ⋅ (p - 1)} ⋅ A ^y

3. 使用费马小定理A ^{x ⋅ (p - 1)} = 1；计算 A ^{(B C)} mod p 变为计算 A ^y

4. 使用 B ^C = x ⋅ (p - 1) + y 然后 y 可以写成 B ^C mod (p - 1)

从上面我们得到 A ^{(B C)} mod p = (A ^y ) mod p

有了所有这些，我们可以分两步计算 A ^{(B C) mod p，同时保持中间结果很小。}

1. y = (B ^C ) mod (p - 1)
2. 结果 = (A ^y ) mod p

例如：2 ^{4 3}模 23

1. y = 4 ³ mod (23 - 1) = 64 mod 22 = 20
2. 结果 = 2 ²⁰模 23 = 1048576 模 23 = 6

问题

我的问题是关于上述转换，我在任何地方都找不到（易于理解的）解释。同样专注于费马小定理也无济于事。可能这些转换应该是显而易见的，但对我来说根本不清楚。

特别是，我不明白为什么指数 B ^C可以表示为 x ⋅ (p - 1) + y。– 这背后的原因是什么？

而且，为什么在使用费马小定理时它应该是“显而易见的” ：

a ^{(p - 1)} ≡ 1 (mod p) 即 A ^{x ⋅ (p - 1)} = 1？

如果有人能以一种易于理解的方式解释这些转变，那就太好了。

我正在根据另一个 tex 文件（报告）的内容创建一个 Beamer 演示文稿。为了避免复制粘贴并允许自动更新内容，我想简单地从原始文件中调用我想要的特定定理，并在 Beamer 演示文稿中我需要的地方重新声明它。由于我想在每个定理之间添加一些额外的解释和示例，因此我需要能够将它们一一导入。此外，我需要两个文档中的定理编号相同，因为演示文稿仅涵盖报告的一部分，例如仅一章。

以下是我发现但不满足我所有要求的类似问题的一些解决方案（我将它们包括在内，以防它们有助于找到解决方案或更好地理解我的问题）：

• 该解决方案的问题在于，我认为它仅适用于同一 pdf/文档中包含的定理：https ://tex.stackexchange.com/questions/51286/recalling-a-theorem
• 下一个的问题是它不允许我一个一个地导入定理。我也不想使用盒子或隐形盒子。此外，在我的情况下，不可能在每个定理的末尾添加附加内容，并且只有在我重述它们时才使其可见（因为由于目标文件是演示文稿，这可能会出现问题）： https ://tex.stackexchange.com/questions/333596/restate-theorem-in-separate-file

以下文件是原始报告的文件：

1. 带有定理 ( theorems.tex ) 的文件：

2. 报告主要文件：

我现在正在做的创建我的演示文稿如下：

如您所见，使用我当前的解决方案，我缺少章节编号参考。我想要的是找到或定义一个类似的命令，\fullref{tex-file}{thm-label}这样我就可以获得相同的结果，但代码类似于：

我的乳胶文档有问题。当我使用下面的代码使用引理时，它会在每个引理的末尾显示一个黑色的小矩形。

代码：

上面的代码显示了下面的输出，

我是 coq 的新手并试图证明这个定理

这是equals的定义

到目前为止，这是我的解决方案

我最终得到了这样的东西

我知道这个输出意味着如果定理必须是正确的，那么命题“Var 0 = Var (S n)”应该遵循命题“false = true”，但我不知道该怎么做并移动继续我的证明。

I know this might be rather out there question but I was curious if it was possible to automatically generate an Isar script given an Isabelle script. My guess is that it should be possible but the problem would be ill-posed as there might be many possible Isar scripts given a tactic script.

My guess of an approach would be something like this:

1. execute the Isabelle tactic script (to reveal many intermediate statements)
2. select with some heuristic H (maybe based on human proofs) of which sub-trees of the proof tree to close with have lemma_sub_tree_i using L1, L2, L3, ..., Ln by SomeProof (perhaps the by ... has more Isar scripts we automatically generated, so this function is recursive)
3. Verify the new Isar script is valid i.e. output the new Isar script if the statement is the same as the original Isabelle tactic proof and the proof goes through/type checks/validates.

Is this possible? At the very least - is it possible in principle with some (hopefully sensible heuristic H. (Of course I know that step 2 is rather important and hoping there is a heuristic that I could truly use in practice to make an actual implementation of this).

Related:

• https://www.reddit.com/r/isabelle/comments/rh0mh7/is_there_an_automatic_way_to_generate_isar/
• https://www.quora.com/unanswered/Is-there-an-automatic-way-to-generate-Isar-scripts-given-a-correct-Isabelle-tactic-script
• https://isabelle.zulipchat.com/#narrow/stream/202967-New-Members.20.26.20Projects/topic/automatic.20isabelle.20-.3E.20Isar.20conversion

我有以下代码：

问题似乎出在最后一步（显示中），编译器告诉我：

我不明白。两种类型不一样吗？

当输入其他两个长度时，我有一个任务要编写一个程序来查找直角三角形的一条边的长度。遇到错误后，我无法让程序继续运行。我希望它在输入不正确的测量值时打印一条消息。但是它停止了，因为它知道能够找到负数的平方根。如何让它覆盖错误？抱歉，如果这令人困惑，我不确定如何完全解释它。

https://linksharing.samsungcloud.com/tPSpRervE2pj