Bottom Line
A
complete formal proof
of the Separation Property of the Chip Model
Proof developed and checked in
Alfa
All definitions are accepted by the termination checker
No bottoms in sight!
Confidence level is high!