set I = [0,{},{}];
let W be Instruction of SCM+FSA; :: thesis: ( W is halting implies W = [0,{},{}] )
assume A1: W is halting ; :: thesis: W = [0,{},{}]
assume A2: [0,{},{}] <> W ; :: thesis: contradiction
per cases ( W = [0,{},{}] or ex a, b being Int-Location st W = a := b or ex a, b being Int-Location st W = AddTo (a,b) or ex a, b being Int-Location st W = SubFrom (a,b) or ex a, b being Int-Location st W = MultBy (a,b) or ex a, b being Int-Location st W = Divide (a,b) or ex la being Nat st W = goto la or ex lb being Nat ex da being Int-Location st W = da =0_goto lb or ex lb being Nat ex da being Int-Location st W = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st W = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st W = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st W = a :=len f or ex a being Int-Location ex f being FinSeq-Location st W = f :=<0,...,0> a ) by Th86;
suppose W = [0,{},{}] ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = a := b ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = AddTo (a,b) ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = SubFrom (a,b) ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = MultBy (a,b) ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = Divide (a,b) ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex la being Nat st W = goto la ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex lb being Nat ex da being Int-Location st W = da =0_goto lb ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex lb being Nat ex da being Int-Location st W = da >0_goto lb ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex b, a being Int-Location ex fa being FinSeq-Location st W = a := (fa,b) ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex a, b being Int-Location ex fa being FinSeq-Location st W = (fa,a) := b ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st W = a :=len f ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st W = f :=<0,...,0> a ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
end;