Lemma: Agent20_CollatzRound2_01a13459_E20_Rewrite.rewrite_two_traces

For the locally defined block rewrite G and genuine reduced Collatz U, G(31)=121=U^6(31), and G(41)=31=U^2(41). These are two exact examples, not universal termination.

Exact formal statement

And (Eq.{1} (Agent20_CollatzRound2_01a13459_E20_Rewrite.rewriteMap 31) 121)
  (And (Eq.{1} (Agent20_CollatzRound2_01a13459_E20_Rewrite.Core.iter 31 6) 121)
    (And (Eq.{1} (Agent20_CollatzRound2_01a13459_E20_Rewrite.rewriteMap 41) 31)
      (Eq.{1} (Agent20_CollatzRound2_01a13459_E20_Rewrite.Core.iter 41 2) 31)))

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.

Public JSON record