t r u e ⇔ { t r u e ⇔ ∅ ⊆ { t r u e , f a l s e , 0 } ⇔ S 0 ⊆ S 1 ∀ i ∈ N ( S i ⊆ S i + 1 ⇒ ∀ t ∈ S i + 1 { t ∈ { t r u e , f a l s e , 0 } ∨ ∃ t 1 ∈ S i t ∈ { s u c c t 1 , p r e d t 1 , i s z e r o t 1 } ∨ ∃ t 1 ∈ S i , t 2 ∈ S i , t 3 ∈ S i t = i f t 1 t h e n t 2 e l s e t 3 ∀ t 1 ∈ S i ( t r u e ⇔ t 1 ∈ S i + 1 ⇒ { s u c c t 1 , p r e d t 1 , i s z e r o t 1 } ⊆ S i + 2 ) ∀ t 1 ∈ S i , t 2 ∈ S i , t 3 ∈ S i ( t r u e ⇔ { t 1 , t 2 , t 3 } ⊆ S i + 1 ⇒ ( i f t 1 t h e n t 2 e l s e t 3 ) ∈ S i + 2 ) ⇒ S i + 1 ⊆ S i + 2 ) ⇒ ∀ i ∈ N S i ⊆ S i + 1 {\displaystyle {\begin{aligned}{\mathit {true}}&\Leftrightarrow \color {CadetBlue}{\begin{cases}\color {black}{\mathit {true}}\Leftrightarrow \varnothing \subseteq \{{\mathsf {true}},{\mathsf {false}},0\}\Leftrightarrow S_{0}\subseteq S_{1}\\{\color {black}{\underset {i\in \mathbb {N} }{\forall }}}\left(\color {black}{\begin{aligned}S_{i}\subseteq S_{i+1}&\Rightarrow {\underset {t\in S_{i+1}}{\forall }}\color {CadetBlue}{\begin{cases}\color {black}\!{\begin{aligned}t\in \{{\mathsf {true}},{\mathsf {false}},0\}\,&\lor {\underset {t_{1}\in S_{i}}{\exists }}t\in \{{\mathsf {succ}}\ t_{1},{\mathsf {pred}}\ t_{1},{\mathsf {iszero}}\ t_{1}\}\\&\lor {\underset {t_{1}\in S_{i},\,t_{2}\in S_{i},\,t_{3}\in S_{i}}{\exists }}t={\mathsf {if}}\ t_{1}\,{\mathsf {then}}\ t_{2}\,{\mathsf {else}}\ t_{3}\end{aligned}}\\{\color {black}{\underset {t_{1}\in S_{i}}{\forall }}}\left(\color {black}{\mathit {true}}\Leftrightarrow t_{1}\in S_{i+1}\Rightarrow \{{\mathsf {succ}}\ t_{1},{\mathsf {pred}}\ t_{1},{\mathsf {iszero}}\ t_{1}\}\subseteq S_{i+2}\right)\\{\color {black}{\underset {t_{1}\in S_{i},\,t_{2}\in S_{i},\,t_{3}\in S_{i}}{\forall }}}\left(\color {black}{\mathit {true}}\Leftrightarrow \{t_{1},t_{2},t_{3}\}\subseteq S_{i+1}\Rightarrow ({\mathsf {if}}\ t_{1}\,{\mathsf {then}}\ t_{2}\,{\mathsf {else}}\ t_{3})\in S_{i+2}\right)\end{cases}}\\&\Rightarrow S_{i+1}\subseteq S_{i+2}\end{aligned}}\right)\end{cases}}\\&\Rightarrow \color {darkgreen}{\underset {i\in \mathbb {N} }{\forall }}S_{i}\subseteq S_{i+1}\end{aligned}}}
sketch of proofs:
∀ s ∈ S ( ∀ r ∈ S ( d e p t h r < d e p t h s ⇒ P r ) ⇒ P s ) ⇔ ∀ n ∈ N ∗ ( ∀ r ∈ S ( d e p t h r < n ⇒ P r ) ⇒ ∀ s ∈ S ( d e p t h s = n ⇒ P s ) ) ⇔ ∀ n ∈ N ∗ ( ∀ m ∈ N ∗ , m < n , s ∈ S ( d e p t h s = m ⇒ P s ) ⇒ ∀ s ∈ S ( d e p t h s = n ⇒ P s ) ) ⇒ ∀ n ∈ N ∗ , s ∈ S ( d e p t h s = n ⇒ P s ) ⇔ ∀ s ∈ S P s {\displaystyle {\begin{aligned}\color {Sepia}{\underset {s\in S}{\forall }}\color {CadetBlue}\left({\color {Sepia}{\underset {r\in S}{\forall }}}\left(\color {Sepia}{\mathit {depth}}\ r<{\mathit {depth}}\ s\Rightarrow Pr\right)\color {Sepia}\Rightarrow Ps\right)&\Leftrightarrow {\underset {n\in \mathbb {N} ^{*}}{\forall }}\color {CadetBlue}\left({\color {black}{\underset {r\in S}{\forall }}}\left(\color {black}{\mathit {depth}}\ r<n\Rightarrow Pr\right){\color {black}\Rightarrow {\underset {s\in S}{\forall }}}\left(\color {black}{\mathit {depth}}\ s=n\Rightarrow Ps\right)\right)\\&\Leftrightarrow {\underset {n\in \mathbb {N} ^{*}}{\forall }}\color {CadetBlue}\left({\color {black}{\underset {m\in \mathbb {N} ^{*},\,m<n,\,s\in S}{\forall }}}\left(\color {black}{\mathit {depth}}\ s=m\Rightarrow Ps\right){\color {black}\Rightarrow {\underset {s\in S}{\forall }}}\left(\color {black}{\mathit {depth}}\ s=n\Rightarrow Ps\right)\right)\\&\Rightarrow {\underset {n\in \mathbb {N} ^{*},\,s\in S}{\forall }}\color {CadetBlue}\left(\color {black}{\mathit {depth}}\ s=n\Rightarrow Ps\right)\color {black}\Leftrightarrow \color {darkgreen}{\underset {s\in S}{\forall }}Ps\end{aligned}}}
∀ s ∈ S ( ∀ r ∈ S ( s i z e r < s i z e s ⇒ P r ) ⇒ P s ) ⇔ ∀ n ∈ N ∗ ( ∀ r ∈ S ( s i z e r < n ⇒ P r ) ⇒ ∀ s ∈ S ( s i z e s = n ⇒ P s ) ) ⇔ ∀ n ∈ N ∗ ( ∀ m ∈ N ∗ , m < n , s ∈ S ( s i z e s = m ⇒ P s ) ⇒ ∀ s ∈ S ( s i z e s = n ⇒ P s ) ) ⇒ ∀ n ∈ N ∗ , s ∈ S ( s i z e s = n ⇒ P s ) ⇔ ∀ s ∈ S P s {\displaystyle {\begin{aligned}\color {Sepia}{\underset {s\in S}{\forall }}\color {CadetBlue}\left({\color {Sepia}{\underset {r\in S}{\forall }}}\left(\color {Sepia}{\mathit {size}}\ r<{\mathit {size}}\ s\Rightarrow Pr\right)\color {Sepia}\Rightarrow Ps\right)&\Leftrightarrow {\underset {n\in \mathbb {N} ^{*}}{\forall }}\color {CadetBlue}\left({\color {black}{\underset {r\in S}{\forall }}}\left(\color {black}{\mathit {size}}\ r<n\Rightarrow Pr\right){\color {black}\Rightarrow {\underset {s\in S}{\forall }}}\left(\color {black}{\mathit {size}}\ s=n\Rightarrow Ps\right)\right)\\&\Leftrightarrow {\underset {n\in \mathbb {N} ^{*}}{\forall }}\color {CadetBlue}\left({\color {black}{\underset {m\in \mathbb {N} ^{*},\,m<n,\,s\in S}{\forall }}}\left(\color {black}{\mathit {size}}\ s=m\Rightarrow Ps\right){\color {black}\Rightarrow {\underset {s\in S}{\forall }}}\left(\color {black}{\mathit {size}}\ s=n\Rightarrow Ps\right)\right)\\&\Rightarrow {\underset {n\in \mathbb {N} ^{*},\,s\in S}{\forall }}\color {CadetBlue}\left(\color {black}{\mathit {size}}\ s=n\Rightarrow Ps\right)\color {black}\Leftrightarrow \color {darkgreen}{\underset {s\in S}{\forall }}Ps\end{aligned}}}
∀ s ∈ S ( ∀ r ( r is a subterm of s ⇒ P r ) ⇒ P s ) ⇒ ∀ i ∈ N ( ∀ j ∈ N , j < i , s ∈ S j P s ⇒ ∀ s ∈ S i P s ) ⇒ ∀ i ∈ N , s ∈ S i P s ⇒ ∀ s ∈ S P s {\displaystyle \color {Sepia}{\underset {s\in S}{\forall }}\color {CadetBlue}\left({\color {Sepia}{\underset {r}{\forall }}}\left(\color {Sepia}r{\text{ is a subterm of }}s\Rightarrow Pr\right)\color {Sepia}\Rightarrow Ps\right)\color {black}\Rightarrow {\underset {i\in \mathbb {N} }{\forall }}\color {CadetBlue}\left(\color {black}{\underset {j\in \mathbb {N} ,\,j<i,\,s\in S_{j}}{\forall }}Ps\Rightarrow {\underset {s\in S_{i}}{\forall }}Ps\right)\color {black}\Rightarrow {\underset {i\in \mathbb {N} ,\,s\in S_{i}}{\forall }}Ps\Rightarrow \color {darkgreen}{\underset {s\in S}{\forall }}Ps}
