55def independentStateAdmitted =
56 (lambda unrestricted slots : Nat .
57 (lambda unrestricted system : (family IndependentStateSystem slots) .
58 (eliminate
59 IndependentStateSystem
60 (lambda unrestricted current : (family IndependentStateSystem slots) . Nat)
61 system
62 (branch
63 IndependentStateSystemOf
64 persistent
65 program
66 initial
67 .
68 (naturalAnd
69 (naturalBelowTwoPower 64 slots)
70 (naturalAnd
71 (naturalNonzero persistent)
72 (naturalAnd
73 (naturalLessOrEqual persistent slots)
74 (naturalAnd
75 (naturalNonzero (stdListLength (family StdList StdU64) initial))
76 (naturalAnd
77 (stdListFold
78 (family StdList StdU64)
79 Nat
80 (lambda unrestricted row : (family StdList StdU64) .
81 (lambda unrestricted rest : Nat .
82 (naturalAnd rest (naturalEqual (stdListLength StdU64 row) slots))))
83 1
84 initial)
85 (stdListFold
86 (family PointwiseAssignment StdU64 slots)
87 Nat
88 (lambda unrestricted assignment : (family PointwiseAssignment StdU64 slots) .
89 (lambda unrestricted rest : Nat .
90 (eliminate
91 PointwiseAssignment
92 (lambda unrestricted current : (family PointwiseAssignment StdU64 slots) .
93 Nat)
94 assignment
95 (branch
96 PointwiseAssign
97 destination
98 expression
99 .
100 (naturalAnd
101 rest
102 (naturalLess (stdFinToNatural slots destination) persistent))))))
103 1
104 program))))))))))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.