@(acc_sem_if_app_guarded STape … (sem_test_char ? (λc:STape.\fst c == bit false))
? (test_char_inv …) (sem_nop …) …)
[| @(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_match) ???)
@(acc_sem_if_app_guarded STape … (sem_test_char ? (λc:STape.\fst c == bit false))
? (test_char_inv …) (sem_nop …) …)
[| @(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_match) ???)