let i1 be Nat; for a being Int-Location holds JUMP (a =0_goto i1) = {i1}
let a be Int-Location; JUMP (a =0_goto i1) = {i1}
set X = { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ;
now for x being object holds
( ( x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ) )let x be
object ;
( ( x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ) )hereby ( x in {i1} implies x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } )
set il1 = 1;
set il2 = 2;
assume A3:
x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum }
;
x in {i1}A4:
NIC (
(a =0_goto i1),2)
= {i1,(2 + 1)}
by Th35;
NIC (
(a =0_goto i1),2)
in { (NIC ((a =0_goto i1),il)) where il is Nat : verum }
;
then
x in NIC (
(a =0_goto i1),2)
by A3, SETFAM_1:def 1;
then A5:
(
x = i1 or
x = 2
+ 1 )
by A4, TARSKI:def 2;
A6:
NIC (
(a =0_goto i1),1)
= {i1,(1 + 1)}
by Th35;
NIC (
(a =0_goto i1),1)
in { (NIC ((a =0_goto i1),il)) where il is Nat : verum }
;
then
x in NIC (
(a =0_goto i1),1)
by A3, SETFAM_1:def 1;
then
(
x = i1 or
x = 1
+ 1 )
by A6, TARSKI:def 2;
hence
x in {i1}
by A5, TARSKI:def 1;
verum
end; assume
x in {i1}
;
x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } then A7:
x = i1
by TARSKI:def 1;
NIC (
(a =0_goto i1),
i1)
in { (NIC ((a =0_goto i1),il)) where il is Nat : verum }
;
hence
x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum }
by A7, A1, SETFAM_1:def 1;
verum end;
hence
JUMP (a =0_goto i1) = {i1}
by TARSKI:2; verum