2 = 1+ 1. 3 = 1+ 2. 4 = 1+ 3. v0 = var# 0. v1 = var# 1. sample-prog: program = (def-label (label# 0) (instr-cons v0 v0 v1 ,instr instr-cons v0 v1 v1 ,instr instr-cons v0 v1 v1 ,instr instr-jump (label# 1))) ,block (def-label (label# 1) (instr-branch-if-nil v1 (label# 2) ,instr instr-fetch-field v1 1 v1 ,instr instr-branch-if-nil v0 (label# 1) ,instr instr-jump (label# 2))) ,block (def-label (label# 2) instr-halt) ,block prog-end. %query 1 1 run-prog sample-prog. sample-ty: program-typing = (block-has-type (label# 0) env0 (block-has-type (label# 1) (var-has-type v0 ty-nil (var-has-type v1 (ty-list ty-nil) env-empty)) (block-has-type (label# 2) env-empty program-typing-empty))). %query 1 1 check-program sample-prog sample-ty. %query 1 1 fast-check-program sample-prog sample-ty.