A precise proof of the n-variable Bekic principle

TL;DR

This paper presents an inductive proof of the n-variable Bekic principle, demonstrating how a vectorial fixpoint of size n can be expressed through nested fixpoints in each coordinate following lexicographic order.

Contribution

It provides a rigorous, inductive proof of the n-variable Bekic principle, clarifying the structure of vectorial fixpoints in formal logic.

Findings

Proof confirms the validity of the n-variable Bekic principle

Nested fixpoints can be systematically constructed for vectorial fixpoints

The approach enhances understanding of fixpoint expressions in formal systems

Abstract

We provide a proof of the $n$-ary Beki\v{c} principle, which states that a vectorial fixpoint of size $n$ can be written in terms of nested fixpoints in each coordinate according to lexicographic order. The proof is inductive.