$(
  @{
    aimeII-2020-p6.0 @e |- ( ph -> T : NN --> QQ ) $@
    aimeII-2020-p6.1 @e |- ( ph -> ( T ` 1 ) = ; 2 0 ) $@
    aimeII-2020-p6.2 @e |- ( ph -> ( T ` 2 ) = ; 2 1 ) $@
    aimeII-2020-p6.3 @e |- ( ph -> N e. NN ) $@
    aimeII-2020-p6.4 @e |- ( ph -> 3 <_ N ) $@
    aimeII-2020-p6.5 @e |- ( ph -> ( T ` N ) = ( ( ( 5 x. ( T ` ( N - 1 ) ) ) + 1 ) / ( ; 2 5 x. ( T ` ( N - 2 ) ) ) ) ) $@
    @( (Contributed by Kunhao Zheng, 12-Aug-2021.) @)
    aimeII-2020-p6 @p |- ( ph -> ( ( denom ` ( T ` ; ; ; 2 0 2 0 ) ) + ( numer ` ( T ` ; ; ; 2 0 2 0 ) ) ) = ; ; 6 2 6 ) @=
      ? @.
  @}
$)