Capture counts are cumulative except occupied slots. Account for every
selected source sequence since the prior durable frontier before encoding.
106def publicationConservation =
107 (lambda unrestricted priorNext : Nat .
108 (lambda unrestricted priorDropped : Nat .
109 (lambda unrestricted priorExcluded : Nat .
110 (lambda unrestricted next : Nat .
111 (lambda unrestricted dropped : Nat .
112 (lambda unrestricted excluded : Nat .
113 (lambda unrestricted occupied : Nat .
114 (naturalAnd
115 (naturalLessOrEqual priorNext next)
116 (naturalAnd
117 (naturalLessOrEqual priorDropped dropped)
118 (naturalAnd
119 (naturalLessOrEqual priorExcluded excluded)
120 (naturalAnd
121 (naturalLessOrEqual
122 (naturalSaturatingSubtract dropped priorDropped)
123 (naturalSaturatingSubtract next priorNext))
124 (naturalEqual
125 occupied
126 (naturalSaturatingSubtract
127 (naturalSaturatingSubtract next priorNext)
128 (naturalSaturatingSubtract dropped priorDropped))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.