этот или фиба?

И это логично

Этот

До фибы мне как до луны

так

Я вот только недавно смотрел, как идрис определяет конечность индуктивного доказательства

Сек дай время мысли сформулирую

Ну идрис молодец

Да там достаточно примитивно - оно кажись всегда должно упрощать выражение при переходе

Вообшем проблема вот в чем интуитивно вполне понятно что после if значения а будут лежать в монотонно возрастаюшей числовой последовательности описываемой как {0;+;3} возникает вопрос как мы это получаем, единственное решение которое пришло мне в голову что мы берем от модуля не диапазон а переодическую последовательность применяем к нейм придекат получаем [true, false, false], 3 , далее применяя этот придекат в качестве фильтра на другую последовательность мы получаем что нам нужно ну тоесть на диапазон {0:+:3}

Проблема вот в чем

Мои размышления интуитивные я не понимаю почему мы получаем переодическую последовательность при модуле а понять это важно потому что это какое то свойство или программы или моей модели не учитывая которое при компресии интервала переменной я могу получитьпроблемы

Компрессию я определили как изменения формы записи набора последовательностей в эквивалентный набор который я называю компактным

Тоесть не содержащим одинаковых значений

Воозможные значения переменной я определил как
num Atomic {
   // Closed interval of natural numbers
   Interval(Interval),
   // Concrete value
   Constant(i64),
   // Regular interval
   Chres(Chres),
   // Periodic sequence
   Periodic((Vec<i64>, i64)),
}

struct Composite(Vec<Atomic>);

impl Composite {
   fn compress(&mut self) {
       todo!();
   }
}

// Defines the set of possible values ​​of a variable
enum Value {
   Atomic(Atomic),
   Composite(Composite),
}

Смотри

Мне кажется, что автоматически эта задача не решается как-то последовательно собственно до систем автоматических доказательств

То есть ты будешь ограничен костылями важнейших случаев

Скажем,
int y = x + 1;
для зависимостей двух переменных

Вроде того, что их разность - константа